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 A V
Assertion dfon2lem7 x x A Tr x x A B A y y B Tr y y B

Proof

Step Hyp Ref Expression
1 dfon2lem7.1 A V
2 elequ1 t = z t t z t
3 elequ2 t = z z t z z
4 2 3 bitrd t = z t t z z
5 4 notbid t = z ¬ t t ¬ z z
6 5 cbvralvw t x ¬ t t z x ¬ z z
7 6 biimpi t x ¬ t t z x ¬ z z
8 7 ralimi x w | w A Tr w t w y y t Tr y y t t x ¬ t t x w | w A Tr w t w y y t Tr y y t z x ¬ z z
9 untuni z w | w A Tr w t w y y t Tr y y t ¬ z z x w | w A Tr w t w y y t Tr y y t z x ¬ z z
10 8 9 sylibr x w | w A Tr w t w y y t Tr y y t t x ¬ t t z w | w A Tr w t w y y t Tr y y t ¬ z z
11 vex x V
12 sseq1 w = x w A x A
13 treq w = x Tr w Tr x
14 raleq w = x t w y y t Tr y y t t x y y t Tr y y t
15 12 13 14 3anbi123d w = x w A Tr w t w y y t Tr y y t x A Tr x t x y y t Tr y y t
16 11 15 elab x w | w A Tr w t w y y t Tr y y t x A Tr x t x y y t Tr y y t
17 vex t V
18 dfon2lem3 t V y y t Tr y y t Tr t u t ¬ u u
19 17 18 ax-mp y y t Tr y y t Tr t u t ¬ u u
20 19 simprd y y t Tr y y t u t ¬ u u
21 untelirr u t ¬ u u ¬ t t
22 20 21 syl y y t Tr y y t ¬ t t
23 22 ralimi t x y y t Tr y y t t x ¬ t t
24 23 3ad2ant3 x A Tr x t x y y t Tr y y t t x ¬ t t
25 16 24 sylbi x w | w A Tr w t w y y t Tr y y t t x ¬ t t
26 10 25 mprg z w | w A Tr w t w y y t Tr y y t ¬ z z
27 untelirr z w | w A Tr w t w y y t Tr y y t ¬ z z ¬ w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t
28 psseq2 t = u y t y u
29 28 anbi1d t = u y t Tr y y u Tr y
30 elequ2 t = u y t y u
31 29 30 imbi12d t = u y t Tr y y t y u Tr y y u
32 31 albidv t = u y y t Tr y y t y y u Tr y y u
33 32 cbvralvw t w y y t Tr y y t u w y y u Tr y y u
34 33 3anbi3i w A Tr w t w y y t Tr y y t w A Tr w u w y y u Tr y y u
35 34 abbii w | w A Tr w t w y y t Tr y y t = w | w A Tr w u w y y u Tr y y u
36 35 unieqi w | w A Tr w t w y y t Tr y y t = w | w A Tr w u w y y u Tr y y u
37 36 eleq2i w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
38 27 37 sylnib z w | w A Tr w t w y y t Tr y y t ¬ z z ¬ w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
39 26 38 ax-mp ¬ w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
40 dfon2lem2 w | w A Tr w t w y y t Tr y y t A
41 1 40 ssexi w | w A Tr w t w y y t Tr y y t V
42 41 snss w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
43 39 42 mtbi ¬ w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
44 43 intnan ¬ w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
45 df-suc suc w | w A Tr w t w y y t Tr y y t = w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t
46 45 sseq1i suc w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
47 unss w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
48 46 47 bitr4i suc w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
49 44 48 mtbir ¬ suc w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
50 41 snss w | w A Tr w t w y y t Tr y y t A w | w A Tr w t w y y t Tr y y t A
51 45 sseq1i suc w | w A Tr w t w y y t Tr y y t A w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t A
52 unss w | w A Tr w t w y y t Tr y y t A w | w A Tr w t w y y t Tr y y t A w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t A
53 51 52 bitr4i suc w | w A Tr w t w y y t Tr y y t A w | w A Tr w t w y y t Tr y y t A w | w A Tr w t w y y t Tr y y t A
54 dfon2lem1 Tr w | w A Tr w t w y y t Tr y y t
55 suctr Tr w | w A Tr w t w y y t Tr y y t Tr suc w | w A Tr w t w y y t Tr y y t
56 54 55 ax-mp Tr suc w | w A Tr w t w y y t Tr y y t
57 vex u V
58 57 elsuc u suc w | w A Tr w t w y y t Tr y y t u w | w A Tr w t w y y t Tr y y t u = w | w A Tr w t w y y t Tr y y t
59 eluni2 u w | w A Tr w t w y y t Tr y y t x w | w A Tr w t w y y t Tr y y t u x
60 nfa1 x x x u Tr x x u
61 32 rspccv t x y y t Tr y y t u x y y u Tr y y u
62 psseq1 y = x y u x u
63 treq y = x Tr y Tr x
64 62 63 anbi12d y = x y u Tr y x u Tr x
65 elequ1 y = x y u x u
66 64 65 imbi12d y = x y u Tr y y u x u Tr x x u
67 66 cbvalvw y y u Tr y y u x x u Tr x x u
68 61 67 syl6ib t x y y t Tr y y t u x x x u Tr x x u
69 68 3ad2ant3 x A Tr x t x y y t Tr y y t u x x x u Tr x x u
70 16 69 sylbi x w | w A Tr w t w y y t Tr y y t u x x x u Tr x x u
71 60 70 rexlimi x w | w A Tr w t w y y t Tr y y t u x x x u Tr x x u
72 59 71 sylbi u w | w A Tr w t w y y t Tr y y t x x u Tr x x u
73 psseq1 y = z y u z u
74 treq y = z Tr y Tr z
75 73 74 anbi12d y = z y u Tr y z u Tr z
76 elequ1 y = z y u z u
77 75 76 imbi12d y = z y u Tr y y u z u Tr z z u
78 77 cbvalvw y y u Tr y y u z z u Tr z z u
79 61 78 syl6ib t x y y t Tr y y t u x z z u Tr z z u
80 79 3ad2ant3 x A Tr x t x y y t Tr y y t u x z z u Tr z z u
81 16 80 sylbi x w | w A Tr w t w y y t Tr y y t u x z z u Tr z z u
82 81 rexlimiv x w | w A Tr w t w y y t Tr y y t u x z z u Tr z z u
83 59 82 sylbi u w | w A Tr w t w y y t Tr y y t z z u Tr z z u
84 83 rgen u w | w A Tr w t w y y t Tr y y t z z u Tr z z u
85 dfon2lem6 Tr w | w A Tr w t w y y t Tr y y t u w | w A Tr w t w y y t Tr y y t z z u Tr z z u x x w | w A Tr w t w y y t Tr y y t Tr x x w | w A Tr w t w y y t Tr y y t
86 54 84 85 mp2an x x w | w A Tr w t w y y t Tr y y t Tr x x w | w A Tr w t w y y t Tr y y t
87 psseq2 u = w | w A Tr w t w y y t Tr y y t x u x w | w A Tr w t w y y t Tr y y t
88 87 anbi1d u = w | w A Tr w t w y y t Tr y y t x u Tr x x w | w A Tr w t w y y t Tr y y t Tr x
89 eleq2 u = w | w A Tr w t w y y t Tr y y t x u x w | w A Tr w t w y y t Tr y y t
90 88 89 imbi12d u = w | w A Tr w t w y y t Tr y y t x u Tr x x u x w | w A Tr w t w y y t Tr y y t Tr x x w | w A Tr w t w y y t Tr y y t
91 90 albidv u = w | w A Tr w t w y y t Tr y y t x x u Tr x x u x x w | w A Tr w t w y y t Tr y y t Tr x x w | w A Tr w t w y y t Tr y y t
92 86 91 mpbiri u = w | w A Tr w t w y y t Tr y y t x x u Tr x x u
93 72 92 jaoi u w | w A Tr w t w y y t Tr y y t u = w | w A Tr w t w y y t Tr y y t x x u Tr x x u
94 58 93 sylbi u suc w | w A Tr w t w y y t Tr y y t x x u Tr x x u
95 94 rgen u suc w | w A Tr w t w y y t Tr y y t x x u Tr x x u
96 41 sucex suc w | w A Tr w t w y y t Tr y y t V
97 sseq1 s = suc w | w A Tr w t w y y t Tr y y t s A suc w | w A Tr w t w y y t Tr y y t A
98 treq s = suc w | w A Tr w t w y y t Tr y y t Tr s Tr suc w | w A Tr w t w y y t Tr y y t
99 raleq s = suc w | w A Tr w t w y y t Tr y y t u s x x u Tr x x u u suc w | w A Tr w t w y y t Tr y y t x x u Tr x x u
100 97 98 99 3anbi123d s = suc w | w A Tr w t w y y t Tr y y t s A Tr s u s x x u Tr x x u suc w | w A Tr w t w y y t Tr y y t A Tr suc w | w A Tr w t w y y t Tr y y t u suc w | w A Tr w t w y y t Tr y y t x x u Tr x x u
101 96 100 elab suc w | w A Tr w t w y y t Tr y y t s | s A Tr s u s x x u Tr x x u suc w | w A Tr w t w y y t Tr y y t A Tr suc w | w A Tr w t w y y t Tr y y t u suc w | w A Tr w t w y y t Tr y y t x x u Tr x x u
102 elssuni suc w | w A Tr w t w y y t Tr y y t s | s A Tr s u s x x u Tr x x u suc w | w A Tr w t w y y t Tr y y t s | s A Tr s u s x x u Tr x x u
103 101 102 sylbir suc w | w A Tr w t w y y t Tr y y t A Tr suc w | w A Tr w t w y y t Tr y y t u suc w | w A Tr w t w y y t Tr y y t x x u Tr x x u suc w | w A Tr w t w y y t Tr y y t s | s A Tr s u s x x u Tr x x u
104 56 95 103 mp3an23 suc w | w A Tr w t w y y t Tr y y t A suc w | w A Tr w t w y y t Tr y y t s | s A Tr s u s x x u Tr x x u
105 sseq1 s = w s A w A
106 treq s = w Tr s Tr w
107 raleq s = w u s x x u Tr x x u u w x x u Tr x x u
108 psseq1 x = y x u y u
109 treq x = y Tr x Tr y
110 108 109 anbi12d x = y x u Tr x y u Tr y
111 elequ1 x = y x u y u
112 110 111 imbi12d x = y x u Tr x x u y u Tr y y u
113 112 cbvalvw x x u Tr x x u y y u Tr y y u
114 113 ralbii u w x x u Tr x x u u w y y u Tr y y u
115 107 114 bitrdi s = w u s x x u Tr x x u u w y y u Tr y y u
116 105 106 115 3anbi123d s = w s A Tr s u s x x u Tr x x u w A Tr w u w y y u Tr y y u
117 116 cbvabv s | s A Tr s u s x x u Tr x x u = w | w A Tr w u w y y u Tr y y u
118 117 unieqi s | s A Tr s u s x x u Tr x x u = w | w A Tr w u w y y u Tr y y u
119 104 118 sseqtrdi suc w | w A Tr w t w y y t Tr y y t A suc w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
120 119 a1i x x A Tr x x A suc w | w A Tr w t w y y t Tr y y t A suc w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
121 53 120 syl5bir x x A Tr x x A w | w A Tr w t w y y t Tr y y t A w | w A Tr w t w y y t Tr y y t A suc w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
122 40 121 mpani x x A Tr x x A w | w A Tr w t w y y t Tr y y t A suc w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
123 50 122 syl5bi x x A Tr x x A w | w A Tr w t w y y t Tr y y t A suc w | w A Tr w t w y y t Tr y y t w | w A Tr w u w y y u Tr y y u
124 49 123 mtoi x x A Tr x x A ¬ w | w A Tr w t w y y t Tr y y t A
125 psseq1 x = w | w A Tr w t w y y t Tr y y t x A w | w A Tr w t w y y t Tr y y t A
126 treq x = w | w A Tr w t w y y t Tr y y t Tr x Tr w | w A Tr w t w y y t Tr y y t
127 125 126 anbi12d x = w | w A Tr w t w y y t Tr y y t x A Tr x w | w A Tr w t w y y t Tr y y t A Tr w | w A Tr w t w y y t Tr y y t
128 eleq1 x = w | w A Tr w t w y y t Tr y y t x A w | w A Tr w t w y y t Tr y y t A
129 127 128 imbi12d x = w | w A Tr w t w y y t Tr y y t x A Tr x x A w | w A Tr w t w y y t Tr y y t A Tr w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t A
130 41 129 spcv x x A Tr x x A w | w A Tr w t w y y t Tr y y t A Tr w | w A Tr w t w y y t Tr y y t w | w A Tr w t w y y t Tr y y t A
131 54 130 mpan2i x x A Tr x x A w | w A Tr w t w y y t Tr y y t A w | w A Tr w t w y y t Tr y y t A
132 124 131 mtod x x A Tr x x A ¬ w | w A Tr w t w y y t Tr y y t A
133 dfpss2 w | w A Tr w t w y y t Tr y y t A w | w A Tr w t w y y t Tr y y t A ¬ w | w A Tr w t w y y t Tr y y t = A
134 133 biimpri w | w A Tr w t w y y t Tr y y t A ¬ w | w A Tr w t w y y t Tr y y t = A w | w A Tr w t w y y t Tr y y t A
135 40 134 mpan ¬ w | w A Tr w t w y y t Tr y y t = A w | w A Tr w t w y y t Tr y y t A
136 132 135 nsyl2 x x A Tr x x A w | w A Tr w t w y y t Tr y y t = A
137 eluni2 z w | w A Tr w t w y y t Tr y y t x w | w A Tr w t w y y t Tr y y t z x
138 psseq2 t = z y t y z
139 138 anbi1d t = z y t Tr y y z Tr y
140 elequ2 t = z y t y z
141 139 140 imbi12d t = z y t Tr y y t y z Tr y y z
142 141 albidv t = z y y t Tr y y t y y z Tr y y z
143 142 cbvralvw t x y y t Tr y y t z x y y z Tr y y z
144 14 143 bitrdi w = x t w y y t Tr y y t z x y y z Tr y y z
145 12 13 144 3anbi123d w = x w A Tr w t w y y t Tr y y t x A Tr x z x y y z Tr y y z
146 11 145 elab x w | w A Tr w t w y y t Tr y y t x A Tr x z x y y z Tr y y z
147 rsp z x y y z Tr y y z z x y y z Tr y y z
148 147 3ad2ant3 x A Tr x z x y y z Tr y y z z x y y z Tr y y z
149 146 148 sylbi x w | w A Tr w t w y y t Tr y y t z x y y z Tr y y z
150 149 rexlimiv x w | w A Tr w t w y y t Tr y y t z x y y z Tr y y z
151 137 150 sylbi z w | w A Tr w t w y y t Tr y y t y y z Tr y y z
152 151 rgen z w | w A Tr w t w y y t Tr y y t y y z Tr y y z
153 raleq w | w A Tr w t w y y t Tr y y t = A z w | w A Tr w t w y y t Tr y y t y y z Tr y y z z A y y z Tr y y z
154 152 153 mpbii w | w A Tr w t w y y t Tr y y t = A z A y y z Tr y y z
155 psseq2 z = B y z y B
156 155 anbi1d z = B y z Tr y y B Tr y
157 eleq2 z = B y z y B
158 156 157 imbi12d z = B y z Tr y y z y B Tr y y B
159 158 albidv z = B y y z Tr y y z y y B Tr y y B
160 159 rspccv z A y y z Tr y y z B A y y B Tr y y B
161 136 154 160 3syl x x A Tr x x A B A y y B Tr y y B