Metamath Proof Explorer


Theorem satffunlem2lem1

Description: Lemma 1 for satffunlem2 . (Contributed by AV, 28-Oct-2023)

Ref Expression
Hypotheses satffunlem2lem1.s S = M Sat E
satffunlem2lem1.a A = M ω 2 nd u 2 nd v
satffunlem2lem1.b B = a M ω | z M i z a ω i 2 nd u
Assertion satffunlem2lem1 Fun S suc N S N S suc N Fun x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A

Proof

Step Hyp Ref Expression
1 satffunlem2lem1.s S = M Sat E
2 satffunlem2lem1.a A = M ω 2 nd u 2 nd v
3 satffunlem2lem1.b B = a M ω | z M i z a ω i 2 nd u
4 simpl u = s v = r u = s
5 4 fveq2d u = s v = r 1 st u = 1 st s
6 simpr u = s v = r v = r
7 6 fveq2d u = s v = r 1 st v = 1 st r
8 5 7 oveq12d u = s v = r 1 st u 𝑔 1 st v = 1 st s 𝑔 1 st r
9 8 eqeq2d u = s v = r x = 1 st u 𝑔 1 st v x = 1 st s 𝑔 1 st r
10 4 fveq2d u = s v = r 2 nd u = 2 nd s
11 6 fveq2d u = s v = r 2 nd v = 2 nd r
12 10 11 ineq12d u = s v = r 2 nd u 2 nd v = 2 nd s 2 nd r
13 12 difeq2d u = s v = r M ω 2 nd u 2 nd v = M ω 2 nd s 2 nd r
14 2 13 syl5eq u = s v = r A = M ω 2 nd s 2 nd r
15 14 eqeq2d u = s v = r y = A y = M ω 2 nd s 2 nd r
16 9 15 anbi12d u = s v = r x = 1 st u 𝑔 1 st v y = A x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
17 16 cbvrexdva u = s v S suc N x = 1 st u 𝑔 1 st v y = A r S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
18 simpr u = s i = j i = j
19 fveq2 u = s 1 st u = 1 st s
20 19 adantr u = s i = j 1 st u = 1 st s
21 18 20 goaleq12d u = s i = j 𝑔 i 1 st u = 𝑔 j 1 st s
22 21 eqeq2d u = s i = j x = 𝑔 i 1 st u x = 𝑔 j 1 st s
23 3 eqeq2i y = B y = a M ω | z M i z a ω i 2 nd u
24 opeq1 i = j i z = j z
25 24 sneqd i = j i z = j z
26 sneq i = j i = j
27 26 difeq2d i = j ω i = ω j
28 27 reseq2d i = j a ω i = a ω j
29 25 28 uneq12d i = j i z a ω i = j z a ω j
30 29 adantl u = s i = j i z a ω i = j z a ω j
31 fveq2 u = s 2 nd u = 2 nd s
32 31 adantr u = s i = j 2 nd u = 2 nd s
33 30 32 eleq12d u = s i = j i z a ω i 2 nd u j z a ω j 2 nd s
34 33 ralbidv u = s i = j z M i z a ω i 2 nd u z M j z a ω j 2 nd s
35 34 rabbidv u = s i = j a M ω | z M i z a ω i 2 nd u = a M ω | z M j z a ω j 2 nd s
36 35 eqeq2d u = s i = j y = a M ω | z M i z a ω i 2 nd u y = a M ω | z M j z a ω j 2 nd s
37 23 36 syl5bb u = s i = j y = B y = a M ω | z M j z a ω j 2 nd s
38 22 37 anbi12d u = s i = j x = 𝑔 i 1 st u y = B x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s
39 38 cbvrexdva u = s i ω x = 𝑔 i 1 st u y = B j ω x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s
40 17 39 orbi12d u = s v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B r S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s
41 40 cbvrexvw u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B s S suc N S N r S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s
42 fveq2 v = r 1 st v = 1 st r
43 19 42 oveqan12d u = s v = r 1 st u 𝑔 1 st v = 1 st s 𝑔 1 st r
44 43 eqeq2d u = s v = r x = 1 st u 𝑔 1 st v x = 1 st s 𝑔 1 st r
45 2 eqeq2i y = A y = M ω 2 nd u 2 nd v
46 fveq2 v = r 2 nd v = 2 nd r
47 31 46 ineqan12d u = s v = r 2 nd u 2 nd v = 2 nd s 2 nd r
48 47 difeq2d u = s v = r M ω 2 nd u 2 nd v = M ω 2 nd s 2 nd r
49 48 eqeq2d u = s v = r y = M ω 2 nd u 2 nd v y = M ω 2 nd s 2 nd r
50 45 49 syl5bb u = s v = r y = A y = M ω 2 nd s 2 nd r
51 44 50 anbi12d u = s v = r x = 1 st u 𝑔 1 st v y = A x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
52 51 cbvrexdva u = s v S suc N S N x = 1 st u 𝑔 1 st v y = A r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
53 52 cbvrexvw u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
54 41 53 orbi12i u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A s S suc N S N r S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
55 simp-5l Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N Fun S suc N
56 eldifi s S suc N S N s S suc N
57 56 adantl Fun S suc N S N S suc N s S suc N S N s S suc N
58 57 anim1i Fun S suc N S N S suc N s S suc N S N r S suc N s S suc N r S suc N
59 58 ad2antrr Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N s S suc N r S suc N
60 eldifi u S suc N S N u S suc N
61 60 adantl Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N u S suc N
62 61 anim1i Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N u S suc N v S suc N
63 55 59 62 3jca Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N Fun S suc N s S suc N r S suc N u S suc N v S suc N
64 id x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
65 2 eqeq2i w = A w = M ω 2 nd u 2 nd v
66 65 biimpi w = A w = M ω 2 nd u 2 nd v
67 66 anim2i x = 1 st u 𝑔 1 st v w = A x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v
68 satffunlem Fun S suc N s S suc N r S suc N u S suc N v S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v y = w
69 63 64 67 68 syl3an Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A y = w
70 69 3exp Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A y = w
71 70 com23 Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
72 71 rexlimdva Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
73 eqeq1 x = 1 st s 𝑔 1 st r x = 𝑔 i 1 st u 1 st s 𝑔 1 st r = 𝑔 i 1 st u
74 fvex 1 st s V
75 fvex 1 st r V
76 gonafv 1 st s V 1 st r V 1 st s 𝑔 1 st r = 1 𝑜 1 st s 1 st r
77 74 75 76 mp2an 1 st s 𝑔 1 st r = 1 𝑜 1 st s 1 st r
78 df-goal 𝑔 i 1 st u = 2 𝑜 i 1 st u
79 77 78 eqeq12i 1 st s 𝑔 1 st r = 𝑔 i 1 st u 1 𝑜 1 st s 1 st r = 2 𝑜 i 1 st u
80 1oex 1 𝑜 V
81 opex 1 st s 1 st r V
82 80 81 opth 1 𝑜 1 st s 1 st r = 2 𝑜 i 1 st u 1 𝑜 = 2 𝑜 1 st s 1 st r = i 1 st u
83 1one2o 1 𝑜 2 𝑜
84 df-ne 1 𝑜 2 𝑜 ¬ 1 𝑜 = 2 𝑜
85 pm2.21 ¬ 1 𝑜 = 2 𝑜 1 𝑜 = 2 𝑜 y = w
86 84 85 sylbi 1 𝑜 2 𝑜 1 𝑜 = 2 𝑜 y = w
87 83 86 ax-mp 1 𝑜 = 2 𝑜 y = w
88 87 adantr 1 𝑜 = 2 𝑜 1 st s 1 st r = i 1 st u y = w
89 82 88 sylbi 1 𝑜 1 st s 1 st r = 2 𝑜 i 1 st u y = w
90 79 89 sylbi 1 st s 𝑔 1 st r = 𝑔 i 1 st u y = w
91 73 90 syl6bi x = 1 st s 𝑔 1 st r x = 𝑔 i 1 st u y = w
92 91 adantr x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 𝑔 i 1 st u y = w
93 92 com12 x = 𝑔 i 1 st u x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
94 93 adantr x = 𝑔 i 1 st u w = B x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
95 94 a1i Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N i ω x = 𝑔 i 1 st u w = B x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
96 95 rexlimdva Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N i ω x = 𝑔 i 1 st u w = B x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
97 72 96 jaod Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
98 97 rexlimdva Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
99 simp-4l Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N Fun S suc N
100 58 adantr Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N s S suc N r S suc N
101 ssel S N S suc N u S N u S suc N
102 101 ad3antlr Fun S suc N S N S suc N s S suc N S N r S suc N u S N u S suc N
103 102 com12 u S N Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N
104 103 adantr u S N v S suc N S N Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N
105 104 impcom Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N u S suc N
106 eldifi v S suc N S N v S suc N
107 106 ad2antll Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N v S suc N
108 105 107 jca Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N u S suc N v S suc N
109 99 100 108 3jca Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N Fun S suc N s S suc N r S suc N u S suc N v S suc N
110 109 64 67 68 syl3an Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A y = w
111 110 3exp Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A y = w
112 111 com23 Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
113 112 rexlimdvva Fun S suc N S N S suc N s S suc N S N r S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
114 98 113 jaod Fun S suc N S N S suc N s S suc N S N r S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = w
115 114 com23 Fun S suc N S N S suc N s S suc N S N r S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
116 115 rexlimdva Fun S suc N S N S suc N s S suc N S N r S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
117 eqeq1 x = 𝑔 j 1 st s x = 1 st u 𝑔 1 st v 𝑔 j 1 st s = 1 st u 𝑔 1 st v
118 df-goal 𝑔 j 1 st s = 2 𝑜 j 1 st s
119 fvex 1 st u V
120 fvex 1 st v V
121 gonafv 1 st u V 1 st v V 1 st u 𝑔 1 st v = 1 𝑜 1 st u 1 st v
122 119 120 121 mp2an 1 st u 𝑔 1 st v = 1 𝑜 1 st u 1 st v
123 118 122 eqeq12i 𝑔 j 1 st s = 1 st u 𝑔 1 st v 2 𝑜 j 1 st s = 1 𝑜 1 st u 1 st v
124 2oex 2 𝑜 V
125 opex j 1 st s V
126 124 125 opth 2 𝑜 j 1 st s = 1 𝑜 1 st u 1 st v 2 𝑜 = 1 𝑜 j 1 st s = 1 st u 1 st v
127 87 eqcoms 2 𝑜 = 1 𝑜 y = w
128 127 adantr 2 𝑜 = 1 𝑜 j 1 st s = 1 st u 1 st v y = w
129 126 128 sylbi 2 𝑜 j 1 st s = 1 𝑜 1 st u 1 st v y = w
130 123 129 sylbi 𝑔 j 1 st s = 1 st u 𝑔 1 st v y = w
131 117 130 syl6bi x = 𝑔 j 1 st s x = 1 st u 𝑔 1 st v y = w
132 131 adantr x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s x = 1 st u 𝑔 1 st v y = w
133 132 com12 x = 1 st u 𝑔 1 st v x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
134 133 adantr x = 1 st u 𝑔 1 st v w = A x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
135 134 rexlimivw v S suc N x = 1 st u 𝑔 1 st v w = A x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
136 135 a1i Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
137 eqeq1 x = 𝑔 i 1 st u x = 𝑔 j 1 st s 𝑔 i 1 st u = 𝑔 j 1 st s
138 78 118 eqeq12i 𝑔 i 1 st u = 𝑔 j 1 st s 2 𝑜 i 1 st u = 2 𝑜 j 1 st s
139 opex i 1 st u V
140 124 139 opth 2 𝑜 i 1 st u = 2 𝑜 j 1 st s 2 𝑜 = 2 𝑜 i 1 st u = j 1 st s
141 vex i V
142 141 119 opth i 1 st u = j 1 st s i = j 1 st u = 1 st s
143 142 anbi2i 2 𝑜 = 2 𝑜 i 1 st u = j 1 st s 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s
144 138 140 143 3bitri 𝑔 i 1 st u = 𝑔 j 1 st s 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s
145 137 144 bitrdi x = 𝑔 i 1 st u x = 𝑔 j 1 st s 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s
146 145 adantl Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i ω x = 𝑔 i 1 st u x = 𝑔 j 1 st s 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s
147 56 a1i Fun S suc N S N S suc N s S suc N S N s S suc N
148 funfv1st2nd Fun S suc N s S suc N S suc N 1 st s = 2 nd s
149 148 ex Fun S suc N s S suc N S suc N 1 st s = 2 nd s
150 149 adantr Fun S suc N S N S suc N s S suc N S suc N 1 st s = 2 nd s
151 funfv1st2nd Fun S suc N u S suc N S suc N 1 st u = 2 nd u
152 151 ex Fun S suc N u S suc N S suc N 1 st u = 2 nd u
153 152 adantr Fun S suc N S N S suc N u S suc N S suc N 1 st u = 2 nd u
154 fveqeq2 1 st u = 1 st s S suc N 1 st u = 2 nd u S suc N 1 st s = 2 nd u
155 eqtr2 S suc N 1 st s = 2 nd u S suc N 1 st s = 2 nd s 2 nd u = 2 nd s
156 29 eqcomd i = j j z a ω j = i z a ω i
157 156 adantl 2 nd u = 2 nd s i = j j z a ω j = i z a ω i
158 simpl 2 nd u = 2 nd s i = j 2 nd u = 2 nd s
159 158 eqcomd 2 nd u = 2 nd s i = j 2 nd s = 2 nd u
160 157 159 eleq12d 2 nd u = 2 nd s i = j j z a ω j 2 nd s i z a ω i 2 nd u
161 160 ralbidv 2 nd u = 2 nd s i = j z M j z a ω j 2 nd s z M i z a ω i 2 nd u
162 161 rabbidv 2 nd u = 2 nd s i = j a M ω | z M j z a ω j 2 nd s = a M ω | z M i z a ω i 2 nd u
163 162 3 eqtr4di 2 nd u = 2 nd s i = j a M ω | z M j z a ω j 2 nd s = B
164 eqeq12 y = a M ω | z M j z a ω j 2 nd s w = B y = w a M ω | z M j z a ω j 2 nd s = B
165 163 164 syl5ibrcom 2 nd u = 2 nd s i = j y = a M ω | z M j z a ω j 2 nd s w = B y = w
166 165 exp4b 2 nd u = 2 nd s i = j y = a M ω | z M j z a ω j 2 nd s w = B y = w
167 155 166 syl S suc N 1 st s = 2 nd u S suc N 1 st s = 2 nd s i = j y = a M ω | z M j z a ω j 2 nd s w = B y = w
168 167 ex S suc N 1 st s = 2 nd u S suc N 1 st s = 2 nd s i = j y = a M ω | z M j z a ω j 2 nd s w = B y = w
169 154 168 syl6bi 1 st u = 1 st s S suc N 1 st u = 2 nd u S suc N 1 st s = 2 nd s i = j y = a M ω | z M j z a ω j 2 nd s w = B y = w
170 169 com24 1 st u = 1 st s i = j S suc N 1 st s = 2 nd s S suc N 1 st u = 2 nd u y = a M ω | z M j z a ω j 2 nd s w = B y = w
171 170 impcom i = j 1 st u = 1 st s S suc N 1 st s = 2 nd s S suc N 1 st u = 2 nd u y = a M ω | z M j z a ω j 2 nd s w = B y = w
172 171 com13 S suc N 1 st u = 2 nd u S suc N 1 st s = 2 nd s i = j 1 st u = 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
173 60 153 172 syl56 Fun S suc N S N S suc N u S suc N S N S suc N 1 st s = 2 nd s i = j 1 st u = 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
174 173 com23 Fun S suc N S N S suc N S suc N 1 st s = 2 nd s u S suc N S N i = j 1 st u = 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
175 147 150 174 3syld Fun S suc N S N S suc N s S suc N S N u S suc N S N i = j 1 st u = 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
176 175 imp Fun S suc N S N S suc N s S suc N S N u S suc N S N i = j 1 st u = 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
177 176 adantr Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i = j 1 st u = 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
178 177 imp Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i = j 1 st u = 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
179 178 adantld Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
180 179 ad2antrr Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i ω x = 𝑔 i 1 st u 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
181 146 180 sylbid Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i ω x = 𝑔 i 1 st u x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
182 181 impd Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i ω x = 𝑔 i 1 st u x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
183 182 ex Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i ω x = 𝑔 i 1 st u x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s w = B y = w
184 183 com34 Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i ω x = 𝑔 i 1 st u w = B x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
185 184 impd Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i ω x = 𝑔 i 1 st u w = B x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
186 185 rexlimdva Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N i ω x = 𝑔 i 1 st u w = B x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
187 136 186 jaod Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
188 187 rexlimdva Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
189 134 a1i Fun S suc N S N S suc N s S suc N S N j ω u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
190 189 rexlimdva Fun S suc N S N S suc N s S suc N S N j ω u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
191 190 rexlimdva Fun S suc N S N S suc N s S suc N S N j ω u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
192 188 191 jaod Fun S suc N S N S suc N s S suc N S N j ω u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s y = w
193 192 com23 Fun S suc N S N S suc N s S suc N S N j ω x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
194 193 rexlimdva Fun S suc N S N S suc N s S suc N S N j ω x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
195 116 194 jaod Fun S suc N S N S suc N s S suc N S N r S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
196 195 rexlimdva Fun S suc N S N S suc N s S suc N S N r S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
197 simplll Fun S suc N S N S suc N s S N r S suc N S N u S suc N S N v S suc N Fun S suc N
198 ssel S N S suc N s S N s S suc N
199 198 adantrd S N S suc N s S N r S suc N S N s S suc N
200 199 adantl Fun S suc N S N S suc N s S N r S suc N S N s S suc N
201 200 imp Fun S suc N S N S suc N s S N r S suc N S N s S suc N
202 eldifi r S suc N S N r S suc N
203 202 ad2antll Fun S suc N S N S suc N s S N r S suc N S N r S suc N
204 201 203 jca Fun S suc N S N S suc N s S N r S suc N S N s S suc N r S suc N
205 204 adantr Fun S suc N S N S suc N s S N r S suc N S N u S suc N S N v S suc N s S suc N r S suc N
206 60 anim1i u S suc N S N v S suc N u S suc N v S suc N
207 206 adantl Fun S suc N S N S suc N s S N r S suc N S N u S suc N S N v S suc N u S suc N v S suc N
208 197 205 207 3jca Fun S suc N S N S suc N s S N r S suc N S N u S suc N S N v S suc N Fun S suc N s S suc N r S suc N u S suc N v S suc N
209 208 adantr Fun S suc N S N S suc N s S N r S suc N S N u S suc N S N v S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A Fun S suc N s S suc N r S suc N u S suc N v S suc N
210 simprl Fun S suc N S N S suc N s S N r S suc N S N u S suc N S N v S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
211 67 ad2antll Fun S suc N S N S suc N s S N r S suc N S N u S suc N S N v S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v
212 209 210 211 68 syl3anc Fun S suc N S N S suc N s S N r S suc N S N u S suc N S N v S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A y = w
213 212 exp32 Fun S suc N S N S suc N s S N r S suc N S N u S suc N S N v S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A y = w
214 213 impancom Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A y = w
215 214 expdimp Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A y = w
216 215 rexlimdv Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A y = w
217 91 adantrd x = 1 st s 𝑔 1 st r x = 𝑔 i 1 st u w = B y = w
218 217 adantr x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 𝑔 i 1 st u w = B y = w
219 218 ad3antlr Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N i ω x = 𝑔 i 1 st u w = B y = w
220 219 rexlimdva Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N i ω x = 𝑔 i 1 st u w = B y = w
221 216 220 jaod Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B y = w
222 221 rexlimdva Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B y = w
223 simplll Fun S suc N S N S suc N s S N r S suc N S N u S N v S suc N S N Fun S suc N
224 204 adantr Fun S suc N S N S suc N s S N r S suc N S N u S N v S suc N S N s S suc N r S suc N
225 101 adantl Fun S suc N S N S suc N u S N u S suc N
226 225 adantr Fun S suc N S N S suc N s S N r S suc N S N u S N u S suc N
227 226 com12 u S N Fun S suc N S N S suc N s S N r S suc N S N u S suc N
228 227 adantr u S N v S suc N S N Fun S suc N S N S suc N s S N r S suc N S N u S suc N
229 228 impcom Fun S suc N S N S suc N s S N r S suc N S N u S N v S suc N S N u S suc N
230 106 ad2antll Fun S suc N S N S suc N s S N r S suc N S N u S N v S suc N S N v S suc N
231 229 230 jca Fun S suc N S N S suc N s S N r S suc N S N u S N v S suc N S N u S suc N v S suc N
232 223 224 231 3jca Fun S suc N S N S suc N s S N r S suc N S N u S N v S suc N S N Fun S suc N s S suc N r S suc N u S suc N v S suc N
233 232 64 67 68 syl3an Fun S suc N S N S suc N s S N r S suc N S N u S N v S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A y = w
234 233 3exp Fun S suc N S N S suc N s S N r S suc N S N u S N v S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r x = 1 st u 𝑔 1 st v w = A y = w
235 234 impancom Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
236 235 rexlimdvv Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
237 222 236 jaod Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
238 237 ex Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
239 238 rexlimdvva Fun S suc N S N S suc N s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
240 196 239 jaod Fun S suc N S N S suc N s S suc N S N r S suc N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = a M ω | z M j z a ω j 2 nd s s S N r S suc N S N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
241 54 240 syl5bi Fun S suc N S N S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
242 241 impd Fun S suc N S N S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
243 242 alrimivv Fun S suc N S N S suc N y w u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
244 eqeq1 y = w y = A w = A
245 244 anbi2d y = w x = 1 st u 𝑔 1 st v y = A x = 1 st u 𝑔 1 st v w = A
246 245 rexbidv y = w v S suc N x = 1 st u 𝑔 1 st v y = A v S suc N x = 1 st u 𝑔 1 st v w = A
247 eqeq1 y = w y = B w = B
248 247 anbi2d y = w x = 𝑔 i 1 st u y = B x = 𝑔 i 1 st u w = B
249 248 rexbidv y = w i ω x = 𝑔 i 1 st u y = B i ω x = 𝑔 i 1 st u w = B
250 246 249 orbi12d y = w v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B
251 250 rexbidv y = w u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B
252 245 2rexbidv y = w u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A
253 251 252 orbi12d y = w u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A
254 253 mo4 * y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A y w u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A u S suc N S N v S suc N x = 1 st u 𝑔 1 st v w = A i ω x = 𝑔 i 1 st u w = B u S N v S suc N S N x = 1 st u 𝑔 1 st v w = A y = w
255 243 254 sylibr Fun S suc N S N S suc N * y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
256 255 alrimiv Fun S suc N S N S suc N x * y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
257 funopab Fun x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A x * y u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A
258 256 257 sylibr Fun S suc N S N S suc N Fun x y | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v y = A i ω x = 𝑔 i 1 st u y = B u S N v S suc N S N x = 1 st u 𝑔 1 st v y = A