Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  tz6.12-afv Structured version   Visualization version   GIF version

Theorem tz6.12-afv 41574
Description: Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 6249. (Contributed by Alexander van der Vekens, 29-Nov-2017.)
Assertion
Ref Expression
tz6.12-afv ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐹

Proof of Theorem tz6.12-afv
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpl 472 . . . . . . . 8 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴 ∈ V)
2 vex 3234 . . . . . . . . 9 𝑦 ∈ V
32a1i 11 . . . . . . . 8 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝑦 ∈ V)
4 df-br 4686 . . . . . . . . . 10 (𝐴𝐹𝑦 ↔ ⟨𝐴, 𝑦⟩ ∈ 𝐹)
54biimpri 218 . . . . . . . . 9 (⟨𝐴, 𝑦⟩ ∈ 𝐹𝐴𝐹𝑦)
65adantl 481 . . . . . . . 8 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴𝐹𝑦)
7 breldmg 5362 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝑦 ∈ V ∧ 𝐴𝐹𝑦) → 𝐴 ∈ dom 𝐹)
81, 3, 6, 7syl3anc 1366 . . . . . . 7 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴 ∈ dom 𝐹)
9 simpl 472 . . . . . . . . 9 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴 ∈ dom 𝐹)
10 velsn 4226 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
11 breq1 4688 . . . . . . . . . . . . . . . . . 18 (𝐴 = 𝑥 → (𝐴𝐹𝑦𝑥𝐹𝑦))
124, 11syl5bbr 274 . . . . . . . . . . . . . . . . 17 (𝐴 = 𝑥 → (⟨𝐴, 𝑦⟩ ∈ 𝐹𝑥𝐹𝑦))
1312eqcoms 2659 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴 → (⟨𝐴, 𝑦⟩ ∈ 𝐹𝑥𝐹𝑦))
1413eubidv 2518 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 ↔ ∃!𝑦 𝑥𝐹𝑦))
1514biimpd 219 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦))
1610, 15sylbi 207 . . . . . . . . . . . . 13 (𝑥 ∈ {𝐴} → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦))
1716com12 32 . . . . . . . . . . . 12 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦))
1817adantl 481 . . . . . . . . . . 11 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦))
1918ralrimiv 2994 . . . . . . . . . 10 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦)
20 fnres 6045 . . . . . . . . . . 11 ((𝐹 ↾ {𝐴}) Fn {𝐴} ↔ ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦)
21 fnfun 6026 . . . . . . . . . . 11 ((𝐹 ↾ {𝐴}) Fn {𝐴} → Fun (𝐹 ↾ {𝐴}))
2220, 21sylbir 225 . . . . . . . . . 10 (∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦 → Fun (𝐹 ↾ {𝐴}))
2319, 22syl 17 . . . . . . . . 9 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → Fun (𝐹 ↾ {𝐴}))
249, 23jca 553 . . . . . . . 8 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
2524ex 449 . . . . . . 7 (𝐴 ∈ dom 𝐹 → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))))
268, 25syl 17 . . . . . 6 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))))
2726impr 648 . . . . 5 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
28 df-dfat 41517 . . . . . 6 (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
29 afvfundmfveq 41539 . . . . . 6 (𝐹 defAt 𝐴 → (𝐹'''𝐴) = (𝐹𝐴))
3028, 29sylbir 225 . . . . 5 ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐹'''𝐴) = (𝐹𝐴))
3127, 30syl 17 . . . 4 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐹'''𝐴) = (𝐹𝐴))
32 tz6.12 6249 . . . . 5 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹𝐴) = 𝑦)
3332adantl 481 . . . 4 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐹𝐴) = 𝑦)
3431, 33eqtrd 2685 . . 3 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐹'''𝐴) = 𝑦)
3534ex 449 . 2 (𝐴 ∈ V → ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦))
36 eu2ndop1stv 41523 . . . . 5 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹𝐴 ∈ V)
3736pm2.24d 147 . . . 4 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (¬ 𝐴 ∈ V → (𝐹'''𝐴) = 𝑦))
3837adantl 481 . . 3 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (¬ 𝐴 ∈ V → (𝐹'''𝐴) = 𝑦))
3938com12 32 . 2 𝐴 ∈ V → ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦))
4035, 39pm2.61i 176 1 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 383   = wceq 1523  wcel 2030  ∃!weu 2498  wral 2941  Vcvv 3231  {csn 4210  cop 4216   class class class wbr 4685  dom cdm 5143  cres 5145  Fun wfun 5920   Fn wfn 5921  cfv 5926   defAt wdfat 41514  '''cafv 41515
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-res 5155  df-iota 5889  df-fun 5928  df-fn 5929  df-fv 5934  df-dfat 41517  df-afv 41518
This theorem is referenced by:  tz6.12-1-afv  41575
  Copyright terms: Public domain W3C validator