Metamath Proof Explorer

Theorem tfrlem13

Description: Lemma for transfinite recursion. If recs is a set function, then C is acceptable, and thus a subset of recs , but dom C is bigger than dom recs . This is a contradiction, so recs must be a proper class function. (Contributed by NM, 14-Aug-1994) (Revised by Mario Carneiro, 14-Nov-2014)

Ref Expression
Hypothesis tfrlem.1 ⊢A=f|∃x∈OnfFnx∧∀y∈xf⁡y=F⁡f↾y
Assertion tfrlem13 ⊢¬recs⁡F∈V

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢A=f|∃x∈OnfFnx∧∀y∈xf⁡y=F⁡f↾y
2 1 tfrlem8 ⊢Ord⁡dom⁡recs⁡F
3 ordirr ⊢Ord⁡dom⁡recs⁡F→¬dom⁡recs⁡F∈dom⁡recs⁡F
4 2 3 ax-mp ⊢¬dom⁡recs⁡F∈dom⁡recs⁡F
5 eqid ⊢recs⁡F∪dom⁡recs⁡FF⁡recs⁡F=recs⁡F∪dom⁡recs⁡FF⁡recs⁡F
6 1 5 tfrlem12 ⊢recs⁡F∈V→recs⁡F∪dom⁡recs⁡FF⁡recs⁡F∈A
7 elssuni ⊢recs⁡F∪dom⁡recs⁡FF⁡recs⁡F∈A→recs⁡F∪dom⁡recs⁡FF⁡recs⁡F⊆⋃A
8 1 recsfval ⊢recs⁡F=⋃A
9 7 8 sseqtrrdi ⊢recs⁡F∪dom⁡recs⁡FF⁡recs⁡F∈A→recs⁡F∪dom⁡recs⁡FF⁡recs⁡F⊆recs⁡F
10 dmss ⊢recs⁡F∪dom⁡recs⁡FF⁡recs⁡F⊆recs⁡F→dom⁡recs⁡F∪dom⁡recs⁡FF⁡recs⁡F⊆dom⁡recs⁡F
11 6 9 10 3syl ⊢recs⁡F∈V→dom⁡recs⁡F∪dom⁡recs⁡FF⁡recs⁡F⊆dom⁡recs⁡F
12 2 a1i ⊢recs⁡F∈V→Ord⁡dom⁡recs⁡F
13 dmexg ⊢recs⁡F∈V→dom⁡recs⁡F∈V
14 elon2 ⊢dom⁡recs⁡F∈On↔Ord⁡dom⁡recs⁡F∧dom⁡recs⁡F∈V
15 12 13 14 sylanbrc ⊢recs⁡F∈V→dom⁡recs⁡F∈On
16 sucidg ⊢dom⁡recs⁡F∈On→dom⁡recs⁡F∈suc⁡dom⁡recs⁡F
17 15 16 syl ⊢recs⁡F∈V→dom⁡recs⁡F∈suc⁡dom⁡recs⁡F
18 1 5 tfrlem10 ⊢dom⁡recs⁡F∈On→recs⁡F∪dom⁡recs⁡FF⁡recs⁡FFnsuc⁡dom⁡recs⁡F
19 fndm ⊢recs⁡F∪dom⁡recs⁡FF⁡recs⁡FFnsuc⁡dom⁡recs⁡F→dom⁡recs⁡F∪dom⁡recs⁡FF⁡recs⁡F=suc⁡dom⁡recs⁡F
20 15 18 19 3syl ⊢recs⁡F∈V→dom⁡recs⁡F∪dom⁡recs⁡FF⁡recs⁡F=suc⁡dom⁡recs⁡F
21 17 20 eleqtrrd ⊢recs⁡F∈V→dom⁡recs⁡F∈dom⁡recs⁡F∪dom⁡recs⁡FF⁡recs⁡F
22 11 21 sseldd ⊢recs⁡F∈V→dom⁡recs⁡F∈dom⁡recs⁡F
23 4 22 mto ⊢¬recs⁡F∈V