Metamath Proof Explorer


Theorem tfr2b

Description: 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, 24-Jun-2015)

Ref Expression
Hypothesis tfr.1 F = recs G
Assertion tfr2b Ord A A dom F F A V

Proof

Step Hyp Ref Expression
1 tfr.1 F = recs G
2 ordeleqon Ord A A On A = On
3 eqid f | x On f Fn x y x f y = G f y = f | x On f Fn x y x f y = G f y
4 3 tfrlem15 A On A dom recs G recs G A V
5 1 dmeqi dom F = dom recs G
6 5 eleq2i A dom F A dom recs G
7 1 reseq1i F A = recs G A
8 7 eleq1i F A V recs G A V
9 4 6 8 3bitr4g A On A dom F F A V
10 onprc ¬ On V
11 elex On dom F On V
12 10 11 mto ¬ On dom F
13 eleq1 A = On A dom F On dom F
14 12 13 mtbiri A = On ¬ A dom F
15 3 tfrlem13 ¬ recs G V
16 1 15 eqneltri ¬ F V
17 reseq2 A = On F A = F On
18 1 tfr1a Fun F Lim dom F
19 18 simpli Fun F
20 funrel Fun F Rel F
21 19 20 ax-mp Rel F
22 18 simpri Lim dom F
23 limord Lim dom F Ord dom F
24 ordsson Ord dom F dom F On
25 22 23 24 mp2b dom F On
26 relssres Rel F dom F On F On = F
27 21 25 26 mp2an F On = F
28 17 27 eqtrdi A = On F A = F
29 28 eleq1d A = On F A V F V
30 16 29 mtbiri A = On ¬ F A V
31 14 30 2falsed A = On A dom F F A V
32 9 31 jaoi A On A = On A dom F F A V
33 2 32 sylbi Ord A A dom F F A V