Metamath Proof Explorer


Theorem satffunlem2lem2

Description: Lemma 2 for satffunlem2 . (Contributed by AV, 27-Oct-2023)

Ref Expression
Hypotheses satffunlem2lem2.s S = M Sat E
satffunlem2lem2.a A = M ω 2 nd u 2 nd v
satffunlem2lem2.b B = a M ω | z M i z a ω i 2 nd u
Assertion satffunlem2lem2 N ω M V E W Fun S suc N dom S suc N dom 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 satffunlem2lem2.s S = M Sat E
2 satffunlem2lem2.a A = M ω 2 nd u 2 nd v
3 satffunlem2lem2.b B = a M ω | z M i z a ω i 2 nd u
4 1 fveq1i S suc N = M Sat E suc N
5 4 dmeqi dom S suc N = dom M Sat E suc N
6 simprl N ω M V E W M V
7 simprr N ω M V E W E W
8 peano2 N ω suc N ω
9 8 adantr N ω M V E W suc N ω
10 6 7 9 3jca N ω M V E W M V E W suc N ω
11 satfdmfmla M V E W suc N ω dom M Sat E suc N = Fmla suc N
12 10 11 syl N ω M V E W dom M Sat E suc N = Fmla suc N
13 12 adantr N ω M V E W Fun S suc N dom M Sat E suc N = Fmla suc N
14 5 13 syl5eq N ω M V E W Fun S suc N dom S suc N = Fmla suc N
15 ovex M ω V
16 15 difexi M ω 2 nd u 2 nd v V
17 2 16 eqeltri A V
18 17 a1i N ω M V E W Fun S suc N u S suc N v S suc N A V
19 18 ralrimiva N ω M V E W Fun S suc N u S suc N v S suc N A V
20 3 15 rabex2 B V
21 20 a1i N ω M V E W Fun S suc N u S suc N i ω B V
22 21 ralrimiva N ω M V E W Fun S suc N u S suc N i ω B V
23 19 22 jca N ω M V E W Fun S suc N u S suc N v S suc N A V i ω B V
24 23 ralrimiva N ω M V E W Fun S suc N u S suc N v S suc N A V i ω B V
25 simplr N ω M V E W Fun S suc N M V E W
26 8 ancri N ω suc N ω N ω
27 26 ad2antrr N ω M V E W Fun S suc N suc N ω N ω
28 25 27 jca N ω M V E W Fun S suc N M V E W suc N ω N ω
29 sssucid N suc N
30 1 satfsschain M V E W suc N ω N ω N suc N S N S suc N
31 28 29 30 mpisyl N ω M V E W Fun S suc N S N S suc N
32 dmopab3rexdif u S suc N v S suc N A V i ω B V S N S suc N dom 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 | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u S N v S suc N S N x = 1 st u 𝑔 1 st v
33 24 31 32 syl2anc N ω M V E W Fun S suc N dom 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 | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u S N v S suc N S N x = 1 st u 𝑔 1 st v
34 simpr N ω M V E W Fun S suc N u M Sat E suc N M Sat E N u M Sat E suc N M Sat E N
35 fveqeq2 w = u 1 st w = 1 st u 1 st u = 1 st u
36 35 adantl N ω M V E W Fun S suc N u M Sat E suc N M Sat E N w = u 1 st w = 1 st u 1 st u = 1 st u
37 eqidd N ω M V E W Fun S suc N u M Sat E suc N M Sat E N 1 st u = 1 st u
38 34 36 37 rspcedvd N ω M V E W Fun S suc N u M Sat E suc N M Sat E N w M Sat E suc N M Sat E N 1 st w = 1 st u
39 4 funeqi Fun S suc N Fun M Sat E suc N
40 39 biimpi Fun S suc N Fun M Sat E suc N
41 40 adantl N ω M V E W Fun S suc N Fun M Sat E suc N
42 1 fveq1i S N = M Sat E N
43 31 42 4 3sstr3g N ω M V E W Fun S suc N M Sat E N M Sat E suc N
44 41 43 jca N ω M V E W Fun S suc N Fun M Sat E suc N M Sat E N M Sat E suc N
45 44 adantr N ω M V E W Fun S suc N u M Sat E suc N M Sat E N Fun M Sat E suc N M Sat E N M Sat E suc N
46 funeldmdif Fun M Sat E suc N M Sat E N M Sat E suc N 1 st u dom M Sat E suc N dom M Sat E N w M Sat E suc N M Sat E N 1 st w = 1 st u
47 45 46 syl N ω M V E W Fun S suc N u M Sat E suc N M Sat E N 1 st u dom M Sat E suc N dom M Sat E N w M Sat E suc N M Sat E N 1 st w = 1 st u
48 38 47 mpbird N ω M V E W Fun S suc N u M Sat E suc N M Sat E N 1 st u dom M Sat E suc N dom M Sat E N
49 48 ex N ω M V E W Fun S suc N u M Sat E suc N M Sat E N 1 st u dom M Sat E suc N dom M Sat E N
50 4 42 difeq12i S suc N S N = M Sat E suc N M Sat E N
51 50 eleq2i u S suc N S N u M Sat E suc N M Sat E N
52 51 a1i N ω M V E W Fun S suc N u S suc N S N u M Sat E suc N M Sat E N
53 13 eqcomd N ω M V E W Fun S suc N Fmla suc N = dom M Sat E suc N
54 simpl N ω M V E W N ω
55 6 7 54 3jca N ω M V E W M V E W N ω
56 satfdmfmla M V E W N ω dom M Sat E N = Fmla N
57 55 56 syl N ω M V E W dom M Sat E N = Fmla N
58 57 eqcomd N ω M V E W Fmla N = dom M Sat E N
59 58 adantr N ω M V E W Fun S suc N Fmla N = dom M Sat E N
60 53 59 difeq12d N ω M V E W Fun S suc N Fmla suc N Fmla N = dom M Sat E suc N dom M Sat E N
61 60 eleq2d N ω M V E W Fun S suc N 1 st u Fmla suc N Fmla N 1 st u dom M Sat E suc N dom M Sat E N
62 49 52 61 3imtr4d N ω M V E W Fun S suc N u S suc N S N 1 st u Fmla suc N Fmla N
63 62 imp N ω M V E W Fun S suc N u S suc N S N 1 st u Fmla suc N Fmla N
64 63 adantr N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u 1 st u Fmla suc N Fmla N
65 oveq1 f = 1 st u f 𝑔 g = 1 st u 𝑔 g
66 65 eqeq2d f = 1 st u x = f 𝑔 g x = 1 st u 𝑔 g
67 66 rexbidv f = 1 st u g Fmla suc N x = f 𝑔 g g Fmla suc N x = 1 st u 𝑔 g
68 eqidd f = 1 st u i = i
69 id f = 1 st u f = 1 st u
70 68 69 goaleq12d f = 1 st u 𝑔 i f = 𝑔 i 1 st u
71 70 eqeq2d f = 1 st u x = 𝑔 i f x = 𝑔 i 1 st u
72 71 rexbidv f = 1 st u i ω x = 𝑔 i f i ω x = 𝑔 i 1 st u
73 67 72 orbi12d f = 1 st u g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f g Fmla suc N x = 1 st u 𝑔 g i ω x = 𝑔 i 1 st u
74 73 adantl N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u f = 1 st u g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f g Fmla suc N x = 1 st u 𝑔 g i ω x = 𝑔 i 1 st u
75 6 adantr N ω M V E W Fun S suc N M V
76 7 adantr N ω M V E W Fun S suc N E W
77 8 ad2antrr N ω M V E W Fun S suc N suc N ω
78 75 76 77 3jca N ω M V E W Fun S suc N M V E W suc N ω
79 satfrel M V E W suc N ω Rel M Sat E suc N
80 78 79 syl N ω M V E W Fun S suc N Rel M Sat E suc N
81 4 releqi Rel S suc N Rel M Sat E suc N
82 80 81 sylibr N ω M V E W Fun S suc N Rel S suc N
83 1stdm Rel S suc N v S suc N 1 st v dom S suc N
84 82 83 sylan N ω M V E W Fun S suc N v S suc N 1 st v dom S suc N
85 14 eqcomd N ω M V E W Fun S suc N Fmla suc N = dom S suc N
86 85 adantr N ω M V E W Fun S suc N v S suc N Fmla suc N = dom S suc N
87 84 86 eleqtrrd N ω M V E W Fun S suc N v S suc N 1 st v Fmla suc N
88 87 ad4ant13 N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v 1 st v Fmla suc N
89 oveq2 g = 1 st v 1 st u 𝑔 g = 1 st u 𝑔 1 st v
90 89 eqeq2d g = 1 st v x = 1 st u 𝑔 g x = 1 st u 𝑔 1 st v
91 90 adantl N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v g = 1 st v x = 1 st u 𝑔 g x = 1 st u 𝑔 1 st v
92 simpr N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v x = 1 st u 𝑔 1 st v
93 88 91 92 rspcedvd N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v g Fmla suc N x = 1 st u 𝑔 g
94 93 rexlimdva2 N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v g Fmla suc N x = 1 st u 𝑔 g
95 94 orim1d N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u g Fmla suc N x = 1 st u 𝑔 g i ω x = 𝑔 i 1 st u
96 95 imp N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u g Fmla suc N x = 1 st u 𝑔 g i ω x = 𝑔 i 1 st u
97 64 74 96 rspcedvd N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f
98 97 rexlimdva2 N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f
99 55 adantr N ω M V E W Fun S suc N M V E W N ω
100 satfrel M V E W N ω Rel M Sat E N
101 99 100 syl N ω M V E W Fun S suc N Rel M Sat E N
102 42 releqi Rel S N Rel M Sat E N
103 101 102 sylibr N ω M V E W Fun S suc N Rel S N
104 1stdm Rel S N u S N 1 st u dom S N
105 103 104 sylan N ω M V E W Fun S suc N u S N 1 st u dom S N
106 42 dmeqi dom S N = dom M Sat E N
107 99 56 syl N ω M V E W Fun S suc N dom M Sat E N = Fmla N
108 106 107 syl5eq N ω M V E W Fun S suc N dom S N = Fmla N
109 108 eqcomd N ω M V E W Fun S suc N Fmla N = dom S N
110 109 adantr N ω M V E W Fun S suc N u S N Fmla N = dom S N
111 105 110 eleqtrrd N ω M V E W Fun S suc N u S N 1 st u Fmla N
112 111 adantr N ω M V E W Fun S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v 1 st u Fmla N
113 66 rexbidv f = 1 st u g Fmla suc N Fmla N x = f 𝑔 g g Fmla suc N Fmla N x = 1 st u 𝑔 g
114 113 adantl N ω M V E W Fun S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v f = 1 st u g Fmla suc N Fmla N x = f 𝑔 g g Fmla suc N Fmla N x = 1 st u 𝑔 g
115 simpr N ω M V E W Fun S suc N v M Sat E suc N M Sat E N v M Sat E suc N M Sat E N
116 fveqeq2 t = v 1 st t = 1 st v 1 st v = 1 st v
117 116 adantl N ω M V E W Fun S suc N v M Sat E suc N M Sat E N t = v 1 st t = 1 st v 1 st v = 1 st v
118 eqidd N ω M V E W Fun S suc N v M Sat E suc N M Sat E N 1 st v = 1 st v
119 115 117 118 rspcedvd N ω M V E W Fun S suc N v M Sat E suc N M Sat E N t M Sat E suc N M Sat E N 1 st t = 1 st v
120 44 adantr N ω M V E W Fun S suc N v M Sat E suc N M Sat E N Fun M Sat E suc N M Sat E N M Sat E suc N
121 funeldmdif Fun M Sat E suc N M Sat E N M Sat E suc N 1 st v dom M Sat E suc N dom M Sat E N t M Sat E suc N M Sat E N 1 st t = 1 st v
122 120 121 syl N ω M V E W Fun S suc N v M Sat E suc N M Sat E N 1 st v dom M Sat E suc N dom M Sat E N t M Sat E suc N M Sat E N 1 st t = 1 st v
123 119 122 mpbird N ω M V E W Fun S suc N v M Sat E suc N M Sat E N 1 st v dom M Sat E suc N dom M Sat E N
124 123 ex N ω M V E W Fun S suc N v M Sat E suc N M Sat E N 1 st v dom M Sat E suc N dom M Sat E N
125 50 eleq2i v S suc N S N v M Sat E suc N M Sat E N
126 125 a1i N ω M V E W Fun S suc N v S suc N S N v M Sat E suc N M Sat E N
127 12 eqcomd N ω M V E W Fmla suc N = dom M Sat E suc N
128 127 58 difeq12d N ω M V E W Fmla suc N Fmla N = dom M Sat E suc N dom M Sat E N
129 128 eleq2d N ω M V E W 1 st v Fmla suc N Fmla N 1 st v dom M Sat E suc N dom M Sat E N
130 129 adantr N ω M V E W Fun S suc N 1 st v Fmla suc N Fmla N 1 st v dom M Sat E suc N dom M Sat E N
131 124 126 130 3imtr4d N ω M V E W Fun S suc N v S suc N S N 1 st v Fmla suc N Fmla N
132 131 adantr N ω M V E W Fun S suc N u S N v S suc N S N 1 st v Fmla suc N Fmla N
133 132 imp N ω M V E W Fun S suc N u S N v S suc N S N 1 st v Fmla suc N Fmla N
134 133 adantr N ω M V E W Fun S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v 1 st v Fmla suc N Fmla N
135 90 adantl N ω M V E W Fun S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v g = 1 st v x = 1 st u 𝑔 g x = 1 st u 𝑔 1 st v
136 simpr N ω M V E W Fun S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v x = 1 st u 𝑔 1 st v
137 134 135 136 rspcedvd N ω M V E W Fun S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v g Fmla suc N Fmla N x = 1 st u 𝑔 g
138 137 r19.29an N ω M V E W Fun S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v g Fmla suc N Fmla N x = 1 st u 𝑔 g
139 112 114 138 rspcedvd N ω M V E W Fun S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v f Fmla N g Fmla suc N Fmla N x = f 𝑔 g
140 139 rexlimdva2 N ω M V E W Fun S suc N u S N v S suc N S N x = 1 st u 𝑔 1 st v f Fmla N g Fmla suc N Fmla N x = f 𝑔 g
141 98 140 orim12d N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u S N v S suc N S N x = 1 st u 𝑔 1 st v f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f f Fmla N g Fmla suc N Fmla N x = f 𝑔 g
142 10 adantr N ω M V E W Fun S suc N M V E W suc N ω
143 11 eqcomd M V E W suc N ω Fmla suc N = dom M Sat E suc N
144 142 143 syl N ω M V E W Fun S suc N Fmla suc N = dom M Sat E suc N
145 107 eqcomd N ω M V E W Fun S suc N Fmla N = dom M Sat E N
146 144 145 difeq12d N ω M V E W Fun S suc N Fmla suc N Fmla N = dom M Sat E suc N dom M Sat E N
147 146 eleq2d N ω M V E W Fun S suc N f Fmla suc N Fmla N f dom M Sat E suc N dom M Sat E N
148 eqid M Sat E = M Sat E
149 148 satfsschain M V E W suc N ω N ω N suc N M Sat E N M Sat E suc N
150 28 29 149 mpisyl N ω M V E W Fun S suc N M Sat E N M Sat E suc N
151 releldmdifi Rel M Sat E suc N M Sat E N M Sat E suc N f dom M Sat E suc N dom M Sat E N u M Sat E suc N M Sat E N 1 st u = f
152 80 150 151 syl2anc N ω M V E W Fun S suc N f dom M Sat E suc N dom M Sat E N u M Sat E suc N M Sat E N 1 st u = f
153 147 152 sylbid N ω M V E W Fun S suc N f Fmla suc N Fmla N u M Sat E suc N M Sat E N 1 st u = f
154 50 eqcomi M Sat E suc N M Sat E N = S suc N S N
155 154 rexeqi u M Sat E suc N M Sat E N 1 st u = f u S suc N S N 1 st u = f
156 r19.41v u S suc N S N 1 st u = f g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f u S suc N S N 1 st u = f g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f
157 oveq1 1 st u = f 1 st u 𝑔 g = f 𝑔 g
158 157 eqeq2d 1 st u = f x = 1 st u 𝑔 g x = f 𝑔 g
159 158 rexbidv 1 st u = f g Fmla suc N x = 1 st u 𝑔 g g Fmla suc N x = f 𝑔 g
160 eqidd 1 st u = f i = i
161 id 1 st u = f 1 st u = f
162 160 161 goaleq12d 1 st u = f 𝑔 i 1 st u = 𝑔 i f
163 162 eqeq2d 1 st u = f x = 𝑔 i 1 st u x = 𝑔 i f
164 163 rexbidv 1 st u = f i ω x = 𝑔 i 1 st u i ω x = 𝑔 i f
165 159 164 orbi12d 1 st u = f g Fmla suc N x = 1 st u 𝑔 g i ω x = 𝑔 i 1 st u g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f
166 165 adantl N ω M V E W Fun S suc N u S suc N S N 1 st u = f g Fmla suc N x = 1 st u 𝑔 g i ω x = 𝑔 i 1 st u g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f
167 142 11 syl N ω M V E W Fun S suc N dom M Sat E suc N = Fmla suc N
168 167 eqcomd N ω M V E W Fun S suc N Fmla suc N = dom M Sat E suc N
169 168 eleq2d N ω M V E W Fun S suc N g Fmla suc N g dom M Sat E suc N
170 releldm2 Rel M Sat E suc N g dom M Sat E suc N v M Sat E suc N 1 st v = g
171 80 170 syl N ω M V E W Fun S suc N g dom M Sat E suc N v M Sat E suc N 1 st v = g
172 169 171 bitrd N ω M V E W Fun S suc N g Fmla suc N v M Sat E suc N 1 st v = g
173 r19.41v v M Sat E suc N 1 st v = g x = 1 st u 𝑔 g v M Sat E suc N 1 st v = g x = 1 st u 𝑔 g
174 1 eqcomi M Sat E = S
175 174 fveq1i M Sat E suc N = S suc N
176 175 rexeqi v M Sat E suc N 1 st v = g x = 1 st u 𝑔 g v S suc N 1 st v = g x = 1 st u 𝑔 g
177 89 eqcoms 1 st v = g 1 st u 𝑔 g = 1 st u 𝑔 1 st v
178 177 eqeq2d 1 st v = g x = 1 st u 𝑔 g x = 1 st u 𝑔 1 st v
179 178 biimpa 1 st v = g x = 1 st u 𝑔 g x = 1 st u 𝑔 1 st v
180 179 a1i N ω M V E W Fun S suc N 1 st v = g x = 1 st u 𝑔 g x = 1 st u 𝑔 1 st v
181 180 reximdv N ω M V E W Fun S suc N v S suc N 1 st v = g x = 1 st u 𝑔 g v S suc N x = 1 st u 𝑔 1 st v
182 176 181 syl5bi N ω M V E W Fun S suc N v M Sat E suc N 1 st v = g x = 1 st u 𝑔 g v S suc N x = 1 st u 𝑔 1 st v
183 173 182 syl5bir N ω M V E W Fun S suc N v M Sat E suc N 1 st v = g x = 1 st u 𝑔 g v S suc N x = 1 st u 𝑔 1 st v
184 183 expd N ω M V E W Fun S suc N v M Sat E suc N 1 st v = g x = 1 st u 𝑔 g v S suc N x = 1 st u 𝑔 1 st v
185 172 184 sylbid N ω M V E W Fun S suc N g Fmla suc N x = 1 st u 𝑔 g v S suc N x = 1 st u 𝑔 1 st v
186 185 rexlimdv N ω M V E W Fun S suc N g Fmla suc N x = 1 st u 𝑔 g v S suc N x = 1 st u 𝑔 1 st v
187 186 ad2antrr N ω M V E W Fun S suc N u S suc N S N 1 st u = f g Fmla suc N x = 1 st u 𝑔 g v S suc N x = 1 st u 𝑔 1 st v
188 187 orim1d N ω M V E W Fun S suc N u S suc N S N 1 st u = f g Fmla suc N x = 1 st u 𝑔 g i ω x = 𝑔 i 1 st u v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
189 166 188 sylbird N ω M V E W Fun S suc N u S suc N S N 1 st u = f g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
190 189 expimpd N ω M V E W Fun S suc N u S suc N S N 1 st u = f g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
191 190 reximdva N ω M V E W Fun S suc N u S suc N S N 1 st u = f g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
192 156 191 syl5bir N ω M V E W Fun S suc N u S suc N S N 1 st u = f g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
193 192 expd N ω M V E W Fun S suc N u S suc N S N 1 st u = f g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
194 155 193 syl5bi N ω M V E W Fun S suc N u M Sat E suc N M Sat E N 1 st u = f g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
195 153 194 syld N ω M V E W Fun S suc N f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
196 195 rexlimdv N ω M V E W Fun S suc N f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
197 145 eleq2d N ω M V E W Fun S suc N f Fmla N f dom M Sat E N
198 55 100 syl N ω M V E W Rel M Sat E N
199 198 adantr N ω M V E W Fun S suc N Rel M Sat E N
200 releldm2 Rel M Sat E N f dom M Sat E N u M Sat E N 1 st u = f
201 199 200 syl N ω M V E W Fun S suc N f dom M Sat E N u M Sat E N 1 st u = f
202 197 201 bitrd N ω M V E W Fun S suc N f Fmla N u M Sat E N 1 st u = f
203 r19.41v u M Sat E N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g u M Sat E N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g
204 42 eqcomi M Sat E N = S N
205 204 rexeqi u M Sat E N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g u S N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g
206 158 rexbidv 1 st u = f g Fmla suc N Fmla N x = 1 st u 𝑔 g g Fmla suc N Fmla N x = f 𝑔 g
207 206 adantl N ω M V E W Fun S suc N 1 st u = f g Fmla suc N Fmla N x = 1 st u 𝑔 g g Fmla suc N Fmla N x = f 𝑔 g
208 146 eleq2d N ω M V E W Fun S suc N g Fmla suc N Fmla N g dom M Sat E suc N dom M Sat E N
209 releldmdifi Rel M Sat E suc N M Sat E N M Sat E suc N g dom M Sat E suc N dom M Sat E N v M Sat E suc N M Sat E N 1 st v = g
210 80 150 209 syl2anc N ω M V E W Fun S suc N g dom M Sat E suc N dom M Sat E N v M Sat E suc N M Sat E N 1 st v = g
211 208 210 sylbid N ω M V E W Fun S suc N g Fmla suc N Fmla N v M Sat E suc N M Sat E N 1 st v = g
212 154 rexeqi v M Sat E suc N M Sat E N 1 st v = g v S suc N S N 1 st v = g
213 178 biimpcd x = 1 st u 𝑔 g 1 st v = g x = 1 st u 𝑔 1 st v
214 213 adantl N ω M V E W Fun S suc N x = 1 st u 𝑔 g 1 st v = g x = 1 st u 𝑔 1 st v
215 214 reximdv N ω M V E W Fun S suc N x = 1 st u 𝑔 g v S suc N S N 1 st v = g v S suc N S N x = 1 st u 𝑔 1 st v
216 215 ex N ω M V E W Fun S suc N x = 1 st u 𝑔 g v S suc N S N 1 st v = g v S suc N S N x = 1 st u 𝑔 1 st v
217 216 com23 N ω M V E W Fun S suc N v S suc N S N 1 st v = g x = 1 st u 𝑔 g v S suc N S N x = 1 st u 𝑔 1 st v
218 212 217 syl5bi N ω M V E W Fun S suc N v M Sat E suc N M Sat E N 1 st v = g x = 1 st u 𝑔 g v S suc N S N x = 1 st u 𝑔 1 st v
219 211 218 syld N ω M V E W Fun S suc N g Fmla suc N Fmla N x = 1 st u 𝑔 g v S suc N S N x = 1 st u 𝑔 1 st v
220 219 rexlimdv N ω M V E W Fun S suc N g Fmla suc N Fmla N x = 1 st u 𝑔 g v S suc N S N x = 1 st u 𝑔 1 st v
221 220 adantr N ω M V E W Fun S suc N 1 st u = f g Fmla suc N Fmla N x = 1 st u 𝑔 g v S suc N S N x = 1 st u 𝑔 1 st v
222 207 221 sylbird N ω M V E W Fun S suc N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g v S suc N S N x = 1 st u 𝑔 1 st v
223 222 expimpd N ω M V E W Fun S suc N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g v S suc N S N x = 1 st u 𝑔 1 st v
224 223 reximdv N ω M V E W Fun S suc N u S N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g u S N v S suc N S N x = 1 st u 𝑔 1 st v
225 205 224 syl5bi N ω M V E W Fun S suc N u M Sat E N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g u S N v S suc N S N x = 1 st u 𝑔 1 st v
226 203 225 syl5bir N ω M V E W Fun S suc N u M Sat E N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g u S N v S suc N S N x = 1 st u 𝑔 1 st v
227 226 expd N ω M V E W Fun S suc N u M Sat E N 1 st u = f g Fmla suc N Fmla N x = f 𝑔 g u S N v S suc N S N x = 1 st u 𝑔 1 st v
228 202 227 sylbid N ω M V E W Fun S suc N f Fmla N g Fmla suc N Fmla N x = f 𝑔 g u S N v S suc N S N x = 1 st u 𝑔 1 st v
229 228 rexlimdv N ω M V E W Fun S suc N f Fmla N g Fmla suc N Fmla N x = f 𝑔 g u S N v S suc N S N x = 1 st u 𝑔 1 st v
230 196 229 orim12d N ω M V E W Fun S suc N f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f f Fmla N g Fmla suc N Fmla N x = f 𝑔 g u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u S N v S suc N S N x = 1 st u 𝑔 1 st v
231 141 230 impbid N ω M V E W Fun S suc N u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u S N v S suc N S N x = 1 st u 𝑔 1 st v f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f f Fmla N g Fmla suc N Fmla N x = f 𝑔 g
232 231 abbidv N ω M V E W Fun S suc N x | u S suc N S N v S suc N x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u u S N v S suc N S N x = 1 st u 𝑔 1 st v = x | f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f f Fmla N g Fmla suc N Fmla N x = f 𝑔 g
233 33 232 eqtrd N ω M V E W Fun S suc N dom 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 | f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f f Fmla N g Fmla suc N Fmla N x = f 𝑔 g
234 14 233 ineq12d N ω M V E W Fun S suc N dom S suc N dom 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 = Fmla suc N x | f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f f Fmla N g Fmla suc N Fmla N x = f 𝑔 g
235 fmlasucdisj N ω Fmla suc N x | f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f f Fmla N g Fmla suc N Fmla N x = f 𝑔 g =
236 235 ad2antrr N ω M V E W Fun S suc N Fmla suc N x | f Fmla suc N Fmla N g Fmla suc N x = f 𝑔 g i ω x = 𝑔 i f f Fmla N g Fmla suc N Fmla N x = f 𝑔 g =
237 234 236 eqtrd N ω M V E W Fun S suc N dom S suc N dom 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 =