Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tfrlem9 Structured version   Visualization version   GIF version

Theorem tfrlem9 7368
 Description: Lemma for transfinite recursion. Here we compute the value of recs (the union of all acceptable functions). (Contributed by NM, 17-Aug-1994.)
Hypothesis
Ref Expression
tfrlem.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Assertion
Ref Expression
tfrlem9 (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))
Distinct variable groups:   𝑥,𝑓,𝑦,𝐵   𝑓,𝐹,𝑥,𝑦
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑓)

Proof of Theorem tfrlem9
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 eldm2g 5242 . . 3 (𝐵 ∈ dom recs(𝐹) → (𝐵 ∈ dom recs(𝐹) ↔ ∃𝑧𝐵, 𝑧⟩ ∈ recs(𝐹)))
21ibi 255 . 2 (𝐵 ∈ dom recs(𝐹) → ∃𝑧𝐵, 𝑧⟩ ∈ recs(𝐹))
3 dfrecs3 7356 . . . . . 6 recs(𝐹) = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
43eleq2i 2680 . . . . 5 (⟨𝐵, 𝑧⟩ ∈ recs(𝐹) ↔ ⟨𝐵, 𝑧⟩ ∈ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))})
5 eluniab 4383 . . . . 5 (⟨𝐵, 𝑧⟩ ∈ {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))} ↔ ∃𝑓(⟨𝐵, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
64, 5bitri 263 . . . 4 (⟨𝐵, 𝑧⟩ ∈ recs(𝐹) ↔ ∃𝑓(⟨𝐵, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))))
7 fnop 5908 . . . . . . . . . . . . . 14 ((𝑓 Fn 𝑥 ∧ ⟨𝐵, 𝑧⟩ ∈ 𝑓) → 𝐵𝑥)
8 rspe 2986 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) → ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
9 tfrlem.1 . . . . . . . . . . . . . . . . . 18 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
109abeq2i 2722 . . . . . . . . . . . . . . . . 17 (𝑓𝐴 ↔ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))))
11 elssuni 4403 . . . . . . . . . . . . . . . . . 18 (𝑓𝐴𝑓 𝐴)
129recsfval 7364 . . . . . . . . . . . . . . . . . 18 recs(𝐹) = 𝐴
1311, 12syl6sseqr 3615 . . . . . . . . . . . . . . . . 17 (𝑓𝐴𝑓 ⊆ recs(𝐹))
1410, 13sylbir 224 . . . . . . . . . . . . . . . 16 (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) → 𝑓 ⊆ recs(𝐹))
158, 14syl 17 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) → 𝑓 ⊆ recs(𝐹))
16 fveq2 6103 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝐵 → (𝑓𝑦) = (𝑓𝐵))
17 reseq2 5312 . . . . . . . . . . . . . . . . . . . . 21 (𝑦 = 𝐵 → (𝑓𝑦) = (𝑓𝐵))
1817fveq2d 6107 . . . . . . . . . . . . . . . . . . . 20 (𝑦 = 𝐵 → (𝐹‘(𝑓𝑦)) = (𝐹‘(𝑓𝐵)))
1916, 18eqeq12d 2625 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝐵 → ((𝑓𝑦) = (𝐹‘(𝑓𝑦)) ↔ (𝑓𝐵) = (𝐹‘(𝑓𝐵))))
2019rspcv 3278 . . . . . . . . . . . . . . . . . 18 (𝐵𝑥 → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) → (𝑓𝐵) = (𝐹‘(𝑓𝐵))))
21 fndm 5904 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 Fn 𝑥 → dom 𝑓 = 𝑥)
2221eleq2d 2673 . . . . . . . . . . . . . . . . . . . 20 (𝑓 Fn 𝑥 → (𝐵 ∈ dom 𝑓𝐵𝑥))
239tfrlem7 7366 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 Fun recs(𝐹)
24 funssfv 6119 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun recs(𝐹) ∧ 𝑓 ⊆ recs(𝐹) ∧ 𝐵 ∈ dom 𝑓) → (recs(𝐹)‘𝐵) = (𝑓𝐵))
2523, 24mp3an1 1403 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ⊆ recs(𝐹) ∧ 𝐵 ∈ dom 𝑓) → (recs(𝐹)‘𝐵) = (𝑓𝐵))
2625adantrl 748 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ⊆ recs(𝐹) ∧ ((𝑓 Fn 𝑥𝑥 ∈ On) ∧ 𝐵 ∈ dom 𝑓)) → (recs(𝐹)‘𝐵) = (𝑓𝐵))
2721eleq1d 2672 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝑓 Fn 𝑥 → (dom 𝑓 ∈ On ↔ 𝑥 ∈ On))
28 onelss 5683 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (dom 𝑓 ∈ On → (𝐵 ∈ dom 𝑓𝐵 ⊆ dom 𝑓))
2927, 28syl6bir 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑓 Fn 𝑥 → (𝑥 ∈ On → (𝐵 ∈ dom 𝑓𝐵 ⊆ dom 𝑓)))
3029imp31 447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝑓 Fn 𝑥𝑥 ∈ On) ∧ 𝐵 ∈ dom 𝑓) → 𝐵 ⊆ dom 𝑓)
31 fun2ssres 5845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((Fun recs(𝐹) ∧ 𝑓 ⊆ recs(𝐹) ∧ 𝐵 ⊆ dom 𝑓) → (recs(𝐹) ↾ 𝐵) = (𝑓𝐵))
3231fveq2d 6107 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((Fun recs(𝐹) ∧ 𝑓 ⊆ recs(𝐹) ∧ 𝐵 ⊆ dom 𝑓) → (𝐹‘(recs(𝐹) ↾ 𝐵)) = (𝐹‘(𝑓𝐵)))
3323, 32mp3an1 1403 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝑓 ⊆ recs(𝐹) ∧ 𝐵 ⊆ dom 𝑓) → (𝐹‘(recs(𝐹) ↾ 𝐵)) = (𝐹‘(𝑓𝐵)))
3430, 33sylan2 490 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑓 ⊆ recs(𝐹) ∧ ((𝑓 Fn 𝑥𝑥 ∈ On) ∧ 𝐵 ∈ dom 𝑓)) → (𝐹‘(recs(𝐹) ↾ 𝐵)) = (𝐹‘(𝑓𝐵)))
3526, 34eqeq12d 2625 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑓 ⊆ recs(𝐹) ∧ ((𝑓 Fn 𝑥𝑥 ∈ On) ∧ 𝐵 ∈ dom 𝑓)) → ((recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)) ↔ (𝑓𝐵) = (𝐹‘(𝑓𝐵))))
3635exbiri 650 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑓 ⊆ recs(𝐹) → (((𝑓 Fn 𝑥𝑥 ∈ On) ∧ 𝐵 ∈ dom 𝑓) → ((𝑓𝐵) = (𝐹‘(𝑓𝐵)) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))
3736com3l 87 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑓 Fn 𝑥𝑥 ∈ On) ∧ 𝐵 ∈ dom 𝑓) → ((𝑓𝐵) = (𝐹‘(𝑓𝐵)) → (𝑓 ⊆ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))
3837exp31 628 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓 Fn 𝑥 → (𝑥 ∈ On → (𝐵 ∈ dom 𝑓 → ((𝑓𝐵) = (𝐹‘(𝑓𝐵)) → (𝑓 ⊆ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))))
3938com34 89 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 Fn 𝑥 → (𝑥 ∈ On → ((𝑓𝐵) = (𝐹‘(𝑓𝐵)) → (𝐵 ∈ dom 𝑓 → (𝑓 ⊆ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))))
4039com24 93 . . . . . . . . . . . . . . . . . . . 20 (𝑓 Fn 𝑥 → (𝐵 ∈ dom 𝑓 → ((𝑓𝐵) = (𝐹‘(𝑓𝐵)) → (𝑥 ∈ On → (𝑓 ⊆ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))))
4122, 40sylbird 249 . . . . . . . . . . . . . . . . . . 19 (𝑓 Fn 𝑥 → (𝐵𝑥 → ((𝑓𝐵) = (𝐹‘(𝑓𝐵)) → (𝑥 ∈ On → (𝑓 ⊆ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))))
4241com3l 87 . . . . . . . . . . . . . . . . . 18 (𝐵𝑥 → ((𝑓𝐵) = (𝐹‘(𝑓𝐵)) → (𝑓 Fn 𝑥 → (𝑥 ∈ On → (𝑓 ⊆ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))))
4320, 42syld 46 . . . . . . . . . . . . . . . . 17 (𝐵𝑥 → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) → (𝑓 Fn 𝑥 → (𝑥 ∈ On → (𝑓 ⊆ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))))
4443com24 93 . . . . . . . . . . . . . . . 16 (𝐵𝑥 → (𝑥 ∈ On → (𝑓 Fn 𝑥 → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) → (𝑓 ⊆ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))))
4544imp4d 616 . . . . . . . . . . . . . . 15 (𝐵𝑥 → ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) → (𝑓 ⊆ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))
4615, 45mpdi 44 . . . . . . . . . . . . . 14 (𝐵𝑥 → ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))))
477, 46syl 17 . . . . . . . . . . . . 13 ((𝑓 Fn 𝑥 ∧ ⟨𝐵, 𝑧⟩ ∈ 𝑓) → ((𝑥 ∈ On ∧ (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))))
4847exp4d 635 . . . . . . . . . . . 12 ((𝑓 Fn 𝑥 ∧ ⟨𝐵, 𝑧⟩ ∈ 𝑓) → (𝑥 ∈ On → (𝑓 Fn 𝑥 → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))))))
4948ex 449 . . . . . . . . . . 11 (𝑓 Fn 𝑥 → (⟨𝐵, 𝑧⟩ ∈ 𝑓 → (𝑥 ∈ On → (𝑓 Fn 𝑥 → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))))
5049com4r 92 . . . . . . . . . 10 (𝑓 Fn 𝑥 → (𝑓 Fn 𝑥 → (⟨𝐵, 𝑧⟩ ∈ 𝑓 → (𝑥 ∈ On → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))))
5150pm2.43i 50 . . . . . . . . 9 (𝑓 Fn 𝑥 → (⟨𝐵, 𝑧⟩ ∈ 𝑓 → (𝑥 ∈ On → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))))))
5251com3l 87 . . . . . . . 8 (⟨𝐵, 𝑧⟩ ∈ 𝑓 → (𝑥 ∈ On → (𝑓 Fn 𝑥 → (∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))))))
5352imp4a 612 . . . . . . 7 (⟨𝐵, 𝑧⟩ ∈ 𝑓 → (𝑥 ∈ On → ((𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))))
5453rexlimdv 3012 . . . . . 6 (⟨𝐵, 𝑧⟩ ∈ 𝑓 → (∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦))) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵))))
5554imp 444 . . . . 5 ((⟨𝐵, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))
5655exlimiv 1845 . . . 4 (∃𝑓(⟨𝐵, 𝑧⟩ ∈ 𝑓 ∧ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))
576, 56sylbi 206 . . 3 (⟨𝐵, 𝑧⟩ ∈ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))
5857exlimiv 1845 . 2 (∃𝑧𝐵, 𝑧⟩ ∈ recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))
592, 58syl 17 1 (𝐵 ∈ dom recs(𝐹) → (recs(𝐹)‘𝐵) = (𝐹‘(recs(𝐹) ↾ 𝐵)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031   = wceq 1475  ∃wex 1695   ∈ wcel 1977  {cab 2596  ∀wral 2896  ∃wrex 2897   ⊆ wss 3540  ⟨cop 4131  ∪ cuni 4372  dom cdm 5038   ↾ cres 5040  Oncon0 5640  Fun wfun 5798   Fn wfn 5799  ‘cfv 5804  recscrecs 7354 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-iota 5768  df-fun 5806  df-fn 5807  df-fv 5812  df-wrecs 7294  df-recs 7355 This theorem is referenced by:  tfrlem11  7371  tfr2a  7378
 Copyright terms: Public domain W3C validator