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 46547
Description: Function value. Theorem 6.12(1) of [TakeutiZaring] p. 27, analogous to tz6.12 6916. (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 482 . . . . . . . 8 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴 ∈ V)
2 vex 3474 . . . . . . . . 9 𝑦 ∈ V
32a1i 11 . . . . . . . 8 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝑦 ∈ V)
4 df-br 5143 . . . . . . . . . 10 (𝐴𝐹𝑦 ↔ ⟨𝐴, 𝑦⟩ ∈ 𝐹)
54biimpri 227 . . . . . . . . 9 (⟨𝐴, 𝑦⟩ ∈ 𝐹𝐴𝐹𝑦)
65adantl 481 . . . . . . . 8 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴𝐹𝑦)
7 breldmg 5906 . . . . . . . 8 ((𝐴 ∈ V ∧ 𝑦 ∈ V ∧ 𝐴𝐹𝑦) → 𝐴 ∈ dom 𝐹)
81, 3, 6, 7syl3anc 1369 . . . . . . 7 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴 ∈ dom 𝐹)
9 simpl 482 . . . . . . . . 9 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → 𝐴 ∈ dom 𝐹)
10 velsn 4640 . . . . . . . . . . . . . 14 (𝑥 ∈ {𝐴} ↔ 𝑥 = 𝐴)
11 breq1 5145 . . . . . . . . . . . . . . . . . 18 (𝐴 = 𝑥 → (𝐴𝐹𝑦𝑥𝐹𝑦))
124, 11bitr3id 285 . . . . . . . . . . . . . . . . 17 (𝐴 = 𝑥 → (⟨𝐴, 𝑦⟩ ∈ 𝐹𝑥𝐹𝑦))
1312eqcoms 2736 . . . . . . . . . . . . . . . 16 (𝑥 = 𝐴 → (⟨𝐴, 𝑦⟩ ∈ 𝐹𝑥𝐹𝑦))
1413eubidv 2576 . . . . . . . . . . . . . . 15 (𝑥 = 𝐴 → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 ↔ ∃!𝑦 𝑥𝐹𝑦))
1514biimpd 228 . . . . . . . . . . . . . 14 (𝑥 = 𝐴 → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦))
1610, 15sylbi 216 . . . . . . . . . . . . 13 (𝑥 ∈ {𝐴} → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → ∃!𝑦 𝑥𝐹𝑦))
1716com12 32 . . . . . . . . . . . 12 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦))
1817adantl 481 . . . . . . . . . . 11 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝑥 ∈ {𝐴} → ∃!𝑦 𝑥𝐹𝑦))
1918ralrimiv 3141 . . . . . . . . . 10 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦)
20 fnres 6676 . . . . . . . . . . 11 ((𝐹 ↾ {𝐴}) Fn {𝐴} ↔ ∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦)
21 fnfun 6648 . . . . . . . . . . 11 ((𝐹 ↾ {𝐴}) Fn {𝐴} → Fun (𝐹 ↾ {𝐴}))
2220, 21sylbir 234 . . . . . . . . . 10 (∀𝑥 ∈ {𝐴}∃!𝑦 𝑥𝐹𝑦 → Fun (𝐹 ↾ {𝐴}))
2319, 22syl 17 . . . . . . . . 9 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → Fun (𝐹 ↾ {𝐴}))
249, 23jca 511 . . . . . . . 8 ((𝐴 ∈ dom 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
2524ex 412 . . . . . . 7 (𝐴 ∈ dom 𝐹 → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))))
268, 25syl 17 . . . . . 6 ((𝐴 ∈ V ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) → (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴}))))
2726impr 454 . . . . 5 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
28 df-dfat 46493 . . . . . 6 (𝐹 defAt 𝐴 ↔ (𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})))
29 afvfundmfveq 46512 . . . . . 6 (𝐹 defAt 𝐴 → (𝐹'''𝐴) = (𝐹𝐴))
3028, 29sylbir 234 . . . . 5 ((𝐴 ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {𝐴})) → (𝐹'''𝐴) = (𝐹𝐴))
3127, 30syl 17 . . . 4 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐹'''𝐴) = (𝐹𝐴))
32 tz6.12 6916 . . . . 5 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹𝐴) = 𝑦)
3332adantl 481 . . . 4 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐹𝐴) = 𝑦)
3431, 33eqtrd 2768 . . 3 ((𝐴 ∈ V ∧ (⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹)) → (𝐹'''𝐴) = 𝑦)
3534ex 412 . 2 (𝐴 ∈ V → ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦))
36 eu2ndop1stv 46499 . . . . 5 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹𝐴 ∈ V)
3736pm2.24d 151 . . . 4 (∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹 → (¬ 𝐴 ∈ V → (𝐹'''𝐴) = 𝑦))
3837adantl 481 . . 3 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (¬ 𝐴 ∈ V → (𝐹'''𝐴) = 𝑦))
3938com12 32 . 2 𝐴 ∈ V → ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦))
4035, 39pm2.61i 182 1 ((⟨𝐴, 𝑦⟩ ∈ 𝐹 ∧ ∃!𝑦𝐴, 𝑦⟩ ∈ 𝐹) → (𝐹'''𝐴) = 𝑦)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395   = wceq 1534  wcel 2099  ∃!weu 2558  wral 3057  Vcvv 3470  {csn 4624  cop 4630   class class class wbr 5142  dom cdm 5672  cres 5674  Fun wfun 6536   Fn wfn 6537  cfv 6542   defAt wdfat 46490  '''cafv 46491
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-sep 5293  ax-nul 5300  ax-pow 5359  ax-pr 5423
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-br 5143  df-opab 5205  df-id 5570  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-res 5684  df-iota 6494  df-fun 6544  df-fn 6545  df-fv 6550  df-aiota 46459  df-dfat 46493  df-afv 46494
This theorem is referenced by:  tz6.12-1-afv  46548
  Copyright terms: Public domain W3C validator