Metamath Proof Explorer


Theorem dfon2lem7

Description: Lemma for dfon2 . All elements of a new ordinal are new ordinals. (Contributed by Scott Fenton, 25-Feb-2011)

Ref Expression
Hypothesis dfon2lem7.1 AV
Assertion dfon2lem7 xxATrxxABAyyBTryyB

Proof

Step Hyp Ref Expression
1 dfon2lem7.1 AV
2 elequ1 t=zttzt
3 elequ2 t=zztzz
4 2 3 bitrd t=zttzz
5 4 notbid t=z¬tt¬zz
6 5 cbvralvw tx¬ttzx¬zz
7 6 biimpi tx¬ttzx¬zz
8 7 ralimi xw|wATrwtwyytTryyttx¬ttxw|wATrwtwyytTryytzx¬zz
9 untuni zw|wATrwtwyytTryyt¬zzxw|wATrwtwyytTryytzx¬zz
10 8 9 sylibr xw|wATrwtwyytTryyttx¬ttzw|wATrwtwyytTryyt¬zz
11 vex xV
12 sseq1 w=xwAxA
13 treq w=xTrwTrx
14 raleq w=xtwyytTryyttxyytTryyt
15 12 13 14 3anbi123d w=xwATrwtwyytTryytxATrxtxyytTryyt
16 11 15 elab xw|wATrwtwyytTryytxATrxtxyytTryyt
17 vex tV
18 dfon2lem3 tVyytTryytTrtut¬uu
19 17 18 ax-mp yytTryytTrtut¬uu
20 19 simprd yytTryytut¬uu
21 untelirr ut¬uu¬tt
22 20 21 syl yytTryyt¬tt
23 22 ralimi txyytTryyttx¬tt
24 23 3ad2ant3 xATrxtxyytTryyttx¬tt
25 16 24 sylbi xw|wATrwtwyytTryyttx¬tt
26 10 25 mprg zw|wATrwtwyytTryyt¬zz
27 untelirr zw|wATrwtwyytTryyt¬zz¬w|wATrwtwyytTryytw|wATrwtwyytTryyt
28 psseq2 t=uytyu
29 28 anbi1d t=uytTryyuTry
30 elequ2 t=uytyu
31 29 30 imbi12d t=uytTryytyuTryyu
32 31 albidv t=uyytTryytyyuTryyu
33 32 cbvralvw twyytTryytuwyyuTryyu
34 33 3anbi3i wATrwtwyytTryytwATrwuwyyuTryyu
35 34 abbii w|wATrwtwyytTryyt=w|wATrwuwyyuTryyu
36 35 unieqi w|wATrwtwyytTryyt=w|wATrwuwyyuTryyu
37 36 eleq2i w|wATrwtwyytTryytw|wATrwtwyytTryytw|wATrwtwyytTryytw|wATrwuwyyuTryyu
38 27 37 sylnib zw|wATrwtwyytTryyt¬zz¬w|wATrwtwyytTryytw|wATrwuwyyuTryyu
39 26 38 ax-mp ¬w|wATrwtwyytTryytw|wATrwuwyyuTryyu
40 dfon2lem2 w|wATrwtwyytTryytA
41 1 40 ssexi w|wATrwtwyytTryytV
42 41 snss w|wATrwtwyytTryytw|wATrwuwyyuTryyuw|wATrwtwyytTryytw|wATrwuwyyuTryyu
43 39 42 mtbi ¬w|wATrwtwyytTryytw|wATrwuwyyuTryyu
44 43 intnan ¬w|wATrwtwyytTryytw|wATrwuwyyuTryyuw|wATrwtwyytTryytw|wATrwuwyyuTryyu
45 df-suc sucw|wATrwtwyytTryyt=w|wATrwtwyytTryytw|wATrwtwyytTryyt
46 45 sseq1i sucw|wATrwtwyytTryytw|wATrwuwyyuTryyuw|wATrwtwyytTryytw|wATrwtwyytTryytw|wATrwuwyyuTryyu
47 unss w|wATrwtwyytTryytw|wATrwuwyyuTryyuw|wATrwtwyytTryytw|wATrwuwyyuTryyuw|wATrwtwyytTryytw|wATrwtwyytTryytw|wATrwuwyyuTryyu
48 46 47 bitr4i sucw|wATrwtwyytTryytw|wATrwuwyyuTryyuw|wATrwtwyytTryytw|wATrwuwyyuTryyuw|wATrwtwyytTryytw|wATrwuwyyuTryyu
49 44 48 mtbir ¬sucw|wATrwtwyytTryytw|wATrwuwyyuTryyu
50 41 snss w|wATrwtwyytTryytAw|wATrwtwyytTryytA
51 45 sseq1i sucw|wATrwtwyytTryytAw|wATrwtwyytTryytw|wATrwtwyytTryytA
52 unss w|wATrwtwyytTryytAw|wATrwtwyytTryytAw|wATrwtwyytTryytw|wATrwtwyytTryytA
53 51 52 bitr4i sucw|wATrwtwyytTryytAw|wATrwtwyytTryytAw|wATrwtwyytTryytA
54 dfon2lem1 Trw|wATrwtwyytTryyt
55 suctr Trw|wATrwtwyytTryytTrsucw|wATrwtwyytTryyt
56 54 55 ax-mp Trsucw|wATrwtwyytTryyt
57 vex uV
58 57 elsuc usucw|wATrwtwyytTryytuw|wATrwtwyytTryytu=w|wATrwtwyytTryyt
59 eluni2 uw|wATrwtwyytTryytxw|wATrwtwyytTryytux
60 nfa1 xxxuTrxxu
61 32 rspccv txyytTryytuxyyuTryyu
62 psseq1 y=xyuxu
63 treq y=xTryTrx
64 62 63 anbi12d y=xyuTryxuTrx
65 elequ1 y=xyuxu
66 64 65 imbi12d y=xyuTryyuxuTrxxu
67 66 cbvalvw yyuTryyuxxuTrxxu
68 61 67 syl6ib txyytTryytuxxxuTrxxu
69 68 3ad2ant3 xATrxtxyytTryytuxxxuTrxxu
70 16 69 sylbi xw|wATrwtwyytTryytuxxxuTrxxu
71 60 70 rexlimi xw|wATrwtwyytTryytuxxxuTrxxu
72 59 71 sylbi uw|wATrwtwyytTryytxxuTrxxu
73 psseq1 y=zyuzu
74 treq y=zTryTrz
75 73 74 anbi12d y=zyuTryzuTrz
76 elequ1 y=zyuzu
77 75 76 imbi12d y=zyuTryyuzuTrzzu
78 77 cbvalvw yyuTryyuzzuTrzzu
79 61 78 syl6ib txyytTryytuxzzuTrzzu
80 79 3ad2ant3 xATrxtxyytTryytuxzzuTrzzu
81 16 80 sylbi xw|wATrwtwyytTryytuxzzuTrzzu
82 81 rexlimiv xw|wATrwtwyytTryytuxzzuTrzzu
83 59 82 sylbi uw|wATrwtwyytTryytzzuTrzzu
84 83 rgen uw|wATrwtwyytTryytzzuTrzzu
85 dfon2lem6 Trw|wATrwtwyytTryytuw|wATrwtwyytTryytzzuTrzzuxxw|wATrwtwyytTryytTrxxw|wATrwtwyytTryyt
86 54 84 85 mp2an xxw|wATrwtwyytTryytTrxxw|wATrwtwyytTryyt
87 psseq2 u=w|wATrwtwyytTryytxuxw|wATrwtwyytTryyt
88 87 anbi1d u=w|wATrwtwyytTryytxuTrxxw|wATrwtwyytTryytTrx
89 eleq2 u=w|wATrwtwyytTryytxuxw|wATrwtwyytTryyt
90 88 89 imbi12d u=w|wATrwtwyytTryytxuTrxxuxw|wATrwtwyytTryytTrxxw|wATrwtwyytTryyt
91 90 albidv u=w|wATrwtwyytTryytxxuTrxxuxxw|wATrwtwyytTryytTrxxw|wATrwtwyytTryyt
92 86 91 mpbiri u=w|wATrwtwyytTryytxxuTrxxu
93 72 92 jaoi uw|wATrwtwyytTryytu=w|wATrwtwyytTryytxxuTrxxu
94 58 93 sylbi usucw|wATrwtwyytTryytxxuTrxxu
95 94 rgen usucw|wATrwtwyytTryytxxuTrxxu
96 41 sucex sucw|wATrwtwyytTryytV
97 sseq1 s=sucw|wATrwtwyytTryytsAsucw|wATrwtwyytTryytA
98 treq s=sucw|wATrwtwyytTryytTrsTrsucw|wATrwtwyytTryyt
99 raleq s=sucw|wATrwtwyytTryytusxxuTrxxuusucw|wATrwtwyytTryytxxuTrxxu
100 97 98 99 3anbi123d s=sucw|wATrwtwyytTryytsATrsusxxuTrxxusucw|wATrwtwyytTryytATrsucw|wATrwtwyytTryytusucw|wATrwtwyytTryytxxuTrxxu
101 96 100 elab sucw|wATrwtwyytTryyts|sATrsusxxuTrxxusucw|wATrwtwyytTryytATrsucw|wATrwtwyytTryytusucw|wATrwtwyytTryytxxuTrxxu
102 elssuni sucw|wATrwtwyytTryyts|sATrsusxxuTrxxusucw|wATrwtwyytTryyts|sATrsusxxuTrxxu
103 101 102 sylbir sucw|wATrwtwyytTryytATrsucw|wATrwtwyytTryytusucw|wATrwtwyytTryytxxuTrxxusucw|wATrwtwyytTryyts|sATrsusxxuTrxxu
104 56 95 103 mp3an23 sucw|wATrwtwyytTryytAsucw|wATrwtwyytTryyts|sATrsusxxuTrxxu
105 sseq1 s=wsAwA
106 treq s=wTrsTrw
107 raleq s=wusxxuTrxxuuwxxuTrxxu
108 psseq1 x=yxuyu
109 treq x=yTrxTry
110 108 109 anbi12d x=yxuTrxyuTry
111 elequ1 x=yxuyu
112 110 111 imbi12d x=yxuTrxxuyuTryyu
113 112 cbvalvw xxuTrxxuyyuTryyu
114 113 ralbii uwxxuTrxxuuwyyuTryyu
115 107 114 bitrdi s=wusxxuTrxxuuwyyuTryyu
116 105 106 115 3anbi123d s=wsATrsusxxuTrxxuwATrwuwyyuTryyu
117 116 cbvabv s|sATrsusxxuTrxxu=w|wATrwuwyyuTryyu
118 117 unieqi s|sATrsusxxuTrxxu=w|wATrwuwyyuTryyu
119 104 118 sseqtrdi sucw|wATrwtwyytTryytAsucw|wATrwtwyytTryytw|wATrwuwyyuTryyu
120 119 a1i xxATrxxAsucw|wATrwtwyytTryytAsucw|wATrwtwyytTryytw|wATrwuwyyuTryyu
121 53 120 syl5bir xxATrxxAw|wATrwtwyytTryytAw|wATrwtwyytTryytAsucw|wATrwtwyytTryytw|wATrwuwyyuTryyu
122 40 121 mpani xxATrxxAw|wATrwtwyytTryytAsucw|wATrwtwyytTryytw|wATrwuwyyuTryyu
123 50 122 syl5bi xxATrxxAw|wATrwtwyytTryytAsucw|wATrwtwyytTryytw|wATrwuwyyuTryyu
124 49 123 mtoi xxATrxxA¬w|wATrwtwyytTryytA
125 psseq1 x=w|wATrwtwyytTryytxAw|wATrwtwyytTryytA
126 treq x=w|wATrwtwyytTryytTrxTrw|wATrwtwyytTryyt
127 125 126 anbi12d x=w|wATrwtwyytTryytxATrxw|wATrwtwyytTryytATrw|wATrwtwyytTryyt
128 eleq1 x=w|wATrwtwyytTryytxAw|wATrwtwyytTryytA
129 127 128 imbi12d x=w|wATrwtwyytTryytxATrxxAw|wATrwtwyytTryytATrw|wATrwtwyytTryytw|wATrwtwyytTryytA
130 41 129 spcv xxATrxxAw|wATrwtwyytTryytATrw|wATrwtwyytTryytw|wATrwtwyytTryytA
131 54 130 mpan2i xxATrxxAw|wATrwtwyytTryytAw|wATrwtwyytTryytA
132 124 131 mtod xxATrxxA¬w|wATrwtwyytTryytA
133 dfpss2 w|wATrwtwyytTryytAw|wATrwtwyytTryytA¬w|wATrwtwyytTryyt=A
134 133 biimpri w|wATrwtwyytTryytA¬w|wATrwtwyytTryyt=Aw|wATrwtwyytTryytA
135 40 134 mpan ¬w|wATrwtwyytTryyt=Aw|wATrwtwyytTryytA
136 132 135 nsyl2 xxATrxxAw|wATrwtwyytTryyt=A
137 eluni2 zw|wATrwtwyytTryytxw|wATrwtwyytTryytzx
138 psseq2 t=zytyz
139 138 anbi1d t=zytTryyzTry
140 elequ2 t=zytyz
141 139 140 imbi12d t=zytTryytyzTryyz
142 141 albidv t=zyytTryytyyzTryyz
143 142 cbvralvw txyytTryytzxyyzTryyz
144 14 143 bitrdi w=xtwyytTryytzxyyzTryyz
145 12 13 144 3anbi123d w=xwATrwtwyytTryytxATrxzxyyzTryyz
146 11 145 elab xw|wATrwtwyytTryytxATrxzxyyzTryyz
147 rsp zxyyzTryyzzxyyzTryyz
148 147 3ad2ant3 xATrxzxyyzTryyzzxyyzTryyz
149 146 148 sylbi xw|wATrwtwyytTryytzxyyzTryyz
150 149 rexlimiv xw|wATrwtwyytTryytzxyyzTryyz
151 137 150 sylbi zw|wATrwtwyytTryytyyzTryyz
152 151 rgen zw|wATrwtwyytTryytyyzTryyz
153 raleq w|wATrwtwyytTryyt=Azw|wATrwtwyytTryytyyzTryyzzAyyzTryyz
154 152 153 mpbii w|wATrwtwyytTryyt=AzAyyzTryyz
155 psseq2 z=ByzyB
156 155 anbi1d z=ByzTryyBTry
157 eleq2 z=ByzyB
158 156 157 imbi12d z=ByzTryyzyBTryyB
159 158 albidv z=ByyzTryyzyyBTryyB
160 159 rspccv zAyyzTryyzBAyyBTryyB
161 136 154 160 3syl xxATrxxABAyyBTryyB