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

Theorem tz6.12-afv2 43964
 Description: Function value (Theorem 6.12(1) of [TakeutiZaring] p. 27), analogous to tz6.12 6678. (Contributed by AV, 5-Sep-2022.)
Assertion
Ref Expression
tz6.12-afv2 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹''''𝐴) = 𝑦)
Distinct variable groups:   𝑦,𝐴   𝑦,𝐹

Proof of Theorem tz6.12-afv2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 simpl 486 . . . . . . . . 9 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴 ∈ V)
2 vex 3445 . . . . . . . . . 10 𝑦 ∈ V
32a1i 11 . . . . . . . . 9 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝑦 ∈ V)
4 df-br 5035 . . . . . . . . . . 11 (𝐴𝐹𝑦 ↔ ⟨𝐴, 𝑦⟩ ∈ 𝐹)
54biimpri 231 . . . . . . . . . 10 (⟨𝐴, 𝑦⟩ ∈ 𝐹𝐴𝐹𝑦)
65adantl 485 . . . . . . . . 9 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴𝐹𝑦)
7 breldmg 5748 . . . . . . . . 9 ((𝐴 ∈ V ∧ 𝑦 ∈ V ∧ 𝐴𝐹𝑦) → 𝐴 ∈ dom 𝐹)
81, 3, 6, 7syl3anc 1368 . . . . . . . 8 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴 ∈ dom 𝐹)
9 simpl 486 . . . . . . . . . 10 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴 ∈ dom 𝐹)
10 velsn 4544 . . . . . . . . . . . . . . 15 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
11 breq1 5037 . . . . . . . . . . . . . . . . . . 19 (𝐴 = 𝑥 → (𝐴𝐹𝑦𝑥𝐹𝑦))
124, 11bitr3id 288 . . . . . . . . . . . . . . . . . 18 (𝐴 = 𝑥 → (⟨𝐴, 𝑦⟩ ∈ 𝐹𝑥𝐹𝑦))
1312eqcoms 2806 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝐴 → (⟨𝐴, 𝑦⟩ ∈ 𝐹𝑥𝐹𝑦))
1413eubidv 2647 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴 → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 ↔ ∃!𝑦 𝑥𝐹𝑦))
1514biimpd 232 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦))
1610, 15sylbi 220 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝐴} → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦))
1716com12 32 . . . . . . . . . . . . 13 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦))
1817adantl 485 . . . . . . . . . . . 12 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦))
1918ralrimiv 3148 . . . . . . . . . . 11 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦)
20 fnres 6454 . . . . . . . . . . . 12 ((𝐹 ↾ {𝐴}) Fn {𝐴} ↔ ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦)
21 fnfun 6431 . . . . . . . . . . . 12 ((𝐹 ↾ {𝐴}) Fn {𝐴} → Fun (𝐹 ↾ {𝐴}))
2220, 21sylbir 238 . . . . . . . . . . 11 (∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦 → Fun (𝐹 ↾ {𝐴}))
2319, 22syl 17 . . . . . . . . . 10 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → Fun (𝐹 ↾ {𝐴}))
249, 23jca 515 . . . . . . . . 9 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
2524ex 416 . . . . . . . 8 (𝐴 ∈ dom 𝐹 → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))))
268, 25syl 17 . . . . . . 7 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))))
2726impr 458 . . . . . 6 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
28 df-dfat 43843 . . . . . 6 (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
2927, 28sylibr 237 . . . . 5 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → 𝐹 defAt 𝐴)
30 dfatafv2iota 43934 . . . . 5 (𝐹 defAt 𝐴 → (𝐹''''𝐴) = (℩𝑦𝐴𝐹𝑦))
3129, 30syl 17 . . . 4 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐹''''𝐴) = (℩𝑦𝐴𝐹𝑦))
324bicomi 227 . . . . . . . . 9 (⟨𝐴, 𝑦⟩ ∈ 𝐹𝐴𝐹𝑦)
3332eubii 2645 . . . . . . . 8 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 ↔ ∃!𝑦 𝐴𝐹𝑦)
3433biimpi 219 . . . . . . 7 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → ∃!𝑦 𝐴𝐹𝑦)
355, 34anim12i 615 . . . . . 6 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦))
3635adantl 485 . . . . 5 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦))
37 iota1 6309 . . . . . 6 (∃!𝑦 𝐴𝐹𝑦 → (𝐴𝐹𝑦 ↔ (℩𝑦𝐴𝐹𝑦) = 𝑦))
3837biimpac 482 . . . . 5 ((𝐴𝐹𝑦 ∧ ∃!𝑦 𝐴𝐹𝑦) → (℩𝑦𝐴𝐹𝑦) = 𝑦)
3936, 38syl 17 . . . 4 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (℩𝑦𝐴𝐹𝑦) = 𝑦)
4031, 39eqtrd 2833 . . 3 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐹''''𝐴) = 𝑦)
4140ex 416 . 2 (𝐴 ∈ V → ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹''''𝐴) = 𝑦))
42 eu2ndop1stv 43849 . . . . 5 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹𝐴 ∈ V)
4342pm2.24d 154 . . . 4 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (¬ 𝐴 ∈ V → (𝐹''''𝐴) = 𝑦))
4443adantl 485 . . 3 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (¬ 𝐴 ∈ V → (𝐹''''𝐴) = 𝑦))
4544com12 32 . 2 𝐴 ∈ V → ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹''''𝐴) = 𝑦))
4641, 45pm2.61i 185 1 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹''''𝐴) = 𝑦)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∃!weu 2628  ∀wral 3106  Vcvv 3442  {csn 4528  ⟨cop 4534   class class class wbr 5034  dom cdm 5523   ↾ cres 5525  ℩cio 6289  Fun wfun 6326   Fn wfn 6327   defAt wdfat 43840  ''''cafv2 43932 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-sbc 3723  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-res 5535  df-iota 6291  df-fun 6334  df-fn 6335  df-dfat 43843  df-afv2 43933 This theorem is referenced by:  tz6.12-1-afv2  43965
 Copyright terms: Public domain W3C validator