Metamath Proof Explorer

Theorem tfrlem15

Description: Lemma for transfinite recursion. Without assuming ax-rep , we can show that all proper initial subsets of recs are sets, while nothing larger is a set. (Contributed by Mario Carneiro, 14-Nov-2014)

Ref Expression
Hypothesis tfrlem.1 ⊢A=f|∃x∈OnfFnx∧∀y∈xf⁡y=F⁡f↾y
Assertion tfrlem15 ⊢B∈On→B∈dom⁡recs⁡F↔recs⁡F↾B∈V

Proof

Step Hyp Ref Expression
1 tfrlem.1 ⊢A=f|∃x∈OnfFnx∧∀y∈xf⁡y=F⁡f↾y
2 1 tfrlem9a ⊢B∈dom⁡recs⁡F→recs⁡F↾B∈V
3 2 adantl ⊢B∈On∧B∈dom⁡recs⁡F→recs⁡F↾B∈V
4 1 tfrlem13 ⊢¬recs⁡F∈V
5 simpr ⊢B∈On∧recs⁡F↾B∈V→recs⁡F↾B∈V
6 resss ⊢recs⁡F↾B⊆recs⁡F
7 6 a1i ⊢dom⁡recs⁡F⊆B→recs⁡F↾B⊆recs⁡F
8 1 tfrlem6 ⊢Rel⁡recs⁡F
9 resdm ⊢Rel⁡recs⁡F→recs⁡F↾dom⁡recs⁡F=recs⁡F
10 8 9 ax-mp ⊢recs⁡F↾dom⁡recs⁡F=recs⁡F
11 ssres2 ⊢dom⁡recs⁡F⊆B→recs⁡F↾dom⁡recs⁡F⊆recs⁡F↾B
12 10 11 eqsstrrid ⊢dom⁡recs⁡F⊆B→recs⁡F⊆recs⁡F↾B
13 7 12 eqssd ⊢dom⁡recs⁡F⊆B→recs⁡F↾B=recs⁡F
14 13 eleq1d ⊢dom⁡recs⁡F⊆B→recs⁡F↾B∈V↔recs⁡F∈V
15 5 14 syl5ibcom ⊢B∈On∧recs⁡F↾B∈V→dom⁡recs⁡F⊆B→recs⁡F∈V
16 4 15 mtoi ⊢B∈On∧recs⁡F↾B∈V→¬dom⁡recs⁡F⊆B
17 1 tfrlem8 ⊢Ord⁡dom⁡recs⁡F
18 eloni ⊢B∈On→Ord⁡B
19 18 adantr ⊢B∈On∧recs⁡F↾B∈V→Ord⁡B
20 ordtri1 ⊢Ord⁡dom⁡recs⁡F∧Ord⁡B→dom⁡recs⁡F⊆B↔¬B∈dom⁡recs⁡F
21 20 con2bid ⊢Ord⁡dom⁡recs⁡F∧Ord⁡B→B∈dom⁡recs⁡F↔¬dom⁡recs⁡F⊆B
22 17 19 21 sylancr ⊢B∈On∧recs⁡F↾B∈V→B∈dom⁡recs⁡F↔¬dom⁡recs⁡F⊆B
23 16 22 mpbird ⊢B∈On∧recs⁡F↾B∈V→B∈dom⁡recs⁡F
24 3 23 impbida ⊢B∈On→B∈dom⁡recs⁡F↔recs⁡F↾B∈V