Metamath Proof Explorer


Theorem satffunlem1lem1

Description: Lemma for satffunlem1 . (Contributed by AV, 17-Oct-2023)

Ref Expression
Assertion satffunlem1lem1 Fun M Sat E N Fun x y | u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u

Proof

Step Hyp Ref Expression
1 fveq2 u = s 1 st u = 1 st s
2 fveq2 v = r 1 st v = 1 st r
3 1 2 oveqan12d u = s v = r 1 st u 𝑔 1 st v = 1 st s 𝑔 1 st r
4 3 eqeq2d u = s v = r x = 1 st u 𝑔 1 st v x = 1 st s 𝑔 1 st r
5 fveq2 u = s 2 nd u = 2 nd s
6 fveq2 v = r 2 nd v = 2 nd r
7 5 6 ineqan12d u = s v = r 2 nd u 2 nd v = 2 nd s 2 nd r
8 7 difeq2d u = s v = r M ω 2 nd u 2 nd v = M ω 2 nd s 2 nd r
9 8 eqeq2d u = s v = r y = M ω 2 nd u 2 nd v y = M ω 2 nd s 2 nd r
10 4 9 anbi12d u = s v = r x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
11 10 cbvrexdva u = s v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v r M Sat E N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r
12 simpr u = s i = j i = j
13 1 adantr u = s i = j 1 st u = 1 st s
14 12 13 goaleq12d u = s i = j 𝑔 i 1 st u = 𝑔 j 1 st s
15 14 eqeq2d u = s i = j x = 𝑔 i 1 st u x = 𝑔 j 1 st s
16 opeq1 i = j i k = j k
17 16 sneqd i = j i k = j k
18 sneq i = j i = j
19 18 difeq2d i = j ω i = ω j
20 19 reseq2d i = j f ω i = f ω j
21 17 20 uneq12d i = j i k f ω i = j k f ω j
22 21 adantl u = s i = j i k f ω i = j k f ω j
23 5 adantr u = s i = j 2 nd u = 2 nd s
24 22 23 eleq12d u = s i = j i k f ω i 2 nd u j k f ω j 2 nd s
25 24 ralbidv u = s i = j k M i k f ω i 2 nd u k M j k f ω j 2 nd s
26 25 rabbidv u = s i = j f M ω | k M i k f ω i 2 nd u = f M ω | k M j k f ω j 2 nd s
27 26 eqeq2d u = s i = j y = f M ω | k M i k f ω i 2 nd u y = f M ω | k M j k f ω j 2 nd s
28 15 27 anbi12d u = s i = j x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s
29 28 cbvrexdva u = s i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u j ω x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s
30 11 29 orbi12d u = s v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u r M Sat E N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s
31 30 cbvrexvw u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u s M Sat E N r M Sat E N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s
32 simp-4l Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N v M Sat E N Fun M Sat E N
33 simpr Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N u M Sat E N
34 33 anim1i Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N v M Sat E N u M Sat E N v M Sat E N
35 simpr Fun M Sat E N s M Sat E N s M Sat E N
36 35 anim1i Fun M Sat E N s M Sat E N r M Sat E N s M Sat E N r M Sat E N
37 36 ad2antrr Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N v M Sat E N s M Sat E N r M Sat E N
38 satffunlem Fun M Sat E N u M Sat E N v M Sat E N s M Sat E N r M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r z = y
39 38 eqcomd Fun M Sat E N u M Sat E N v M Sat E N s M Sat E N r M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
40 39 3exp Fun M Sat E N u M Sat E N v M Sat E N s M Sat E N r M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
41 32 34 37 40 syl3anc Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
42 41 rexlimdva Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
43 eqeq1 x = 𝑔 i 1 st u x = 1 st s 𝑔 1 st r 𝑔 i 1 st u = 1 st s 𝑔 1 st r
44 df-goal 𝑔 i 1 st u = 2 𝑜 i 1 st u
45 fvex 1 st s V
46 fvex 1 st r V
47 gonafv 1 st s V 1 st r V 1 st s 𝑔 1 st r = 1 𝑜 1 st s 1 st r
48 45 46 47 mp2an 1 st s 𝑔 1 st r = 1 𝑜 1 st s 1 st r
49 44 48 eqeq12i 𝑔 i 1 st u = 1 st s 𝑔 1 st r 2 𝑜 i 1 st u = 1 𝑜 1 st s 1 st r
50 2oex 2 𝑜 V
51 opex i 1 st u V
52 50 51 opth 2 𝑜 i 1 st u = 1 𝑜 1 st s 1 st r 2 𝑜 = 1 𝑜 i 1 st u = 1 st s 1 st r
53 1one2o 1 𝑜 2 𝑜
54 df-ne 1 𝑜 2 𝑜 ¬ 1 𝑜 = 2 𝑜
55 pm2.21 ¬ 1 𝑜 = 2 𝑜 1 𝑜 = 2 𝑜 y = M ω 2 nd s 2 nd r y = z
56 54 55 sylbi 1 𝑜 2 𝑜 1 𝑜 = 2 𝑜 y = M ω 2 nd s 2 nd r y = z
57 53 56 ax-mp 1 𝑜 = 2 𝑜 y = M ω 2 nd s 2 nd r y = z
58 57 eqcoms 2 𝑜 = 1 𝑜 y = M ω 2 nd s 2 nd r y = z
59 58 adantr 2 𝑜 = 1 𝑜 i 1 st u = 1 st s 1 st r y = M ω 2 nd s 2 nd r y = z
60 52 59 sylbi 2 𝑜 i 1 st u = 1 𝑜 1 st s 1 st r y = M ω 2 nd s 2 nd r y = z
61 49 60 sylbi 𝑔 i 1 st u = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
62 43 61 syl6bi x = 𝑔 i 1 st u x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
63 62 impd x = 𝑔 i 1 st u x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
64 63 adantr x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
65 64 a1i Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
66 65 rexlimdva Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
67 42 66 jaod Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
68 67 rexlimdva Fun M Sat E N s M Sat E N r M Sat E N u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r y = z
69 68 com23 Fun M Sat E N s M Sat E N r M Sat E N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
70 69 rexlimdva Fun M Sat E N s M Sat E N r M Sat E N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
71 eqeq1 x = 𝑔 j 1 st s x = 1 st u 𝑔 1 st v 𝑔 j 1 st s = 1 st u 𝑔 1 st v
72 df-goal 𝑔 j 1 st s = 2 𝑜 j 1 st s
73 fvex 1 st u V
74 fvex 1 st v V
75 gonafv 1 st u V 1 st v V 1 st u 𝑔 1 st v = 1 𝑜 1 st u 1 st v
76 73 74 75 mp2an 1 st u 𝑔 1 st v = 1 𝑜 1 st u 1 st v
77 72 76 eqeq12i 𝑔 j 1 st s = 1 st u 𝑔 1 st v 2 𝑜 j 1 st s = 1 𝑜 1 st u 1 st v
78 opex j 1 st s V
79 50 78 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
80 pm2.21 ¬ 1 𝑜 = 2 𝑜 1 𝑜 = 2 𝑜 y = z
81 54 80 sylbi 1 𝑜 2 𝑜 1 𝑜 = 2 𝑜 y = z
82 53 81 ax-mp 1 𝑜 = 2 𝑜 y = z
83 82 eqcoms 2 𝑜 = 1 𝑜 y = z
84 83 adantr 2 𝑜 = 1 𝑜 j 1 st s = 1 st u 1 st v y = z
85 79 84 sylbi 2 𝑜 j 1 st s = 1 𝑜 1 st u 1 st v y = z
86 77 85 sylbi 𝑔 j 1 st s = 1 st u 𝑔 1 st v y = z
87 71 86 syl6bi x = 𝑔 j 1 st s x = 1 st u 𝑔 1 st v y = z
88 87 adantr x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s x = 1 st u 𝑔 1 st v y = z
89 88 com12 x = 1 st u 𝑔 1 st v x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s y = z
90 89 adantr x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s y = z
91 90 a1i Fun M Sat E N s M Sat E N j ω u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s y = z
92 91 rexlimdva Fun M Sat E N s M Sat E N j ω u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s y = z
93 eqeq1 x = 𝑔 i 1 st u x = 𝑔 j 1 st s 𝑔 i 1 st u = 𝑔 j 1 st s
94 44 72 eqeq12i 𝑔 i 1 st u = 𝑔 j 1 st s 2 𝑜 i 1 st u = 2 𝑜 j 1 st s
95 50 51 opth 2 𝑜 i 1 st u = 2 𝑜 j 1 st s 2 𝑜 = 2 𝑜 i 1 st u = j 1 st s
96 vex i V
97 96 73 opth i 1 st u = j 1 st s i = j 1 st u = 1 st s
98 97 anbi2i 2 𝑜 = 2 𝑜 i 1 st u = j 1 st s 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s
99 94 95 98 3bitri 𝑔 i 1 st u = 𝑔 j 1 st s 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s
100 93 99 bitrdi x = 𝑔 i 1 st u x = 𝑔 j 1 st s 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s
101 100 adantl Fun M Sat E N s M Sat E N j ω u M Sat E N i ω x = 𝑔 i 1 st u x = 𝑔 j 1 st s 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s
102 funfv1st2nd Fun M Sat E N s M Sat E N M Sat E N 1 st s = 2 nd s
103 102 ex Fun M Sat E N s M Sat E N M Sat E N 1 st s = 2 nd s
104 funfv1st2nd Fun M Sat E N u M Sat E N M Sat E N 1 st u = 2 nd u
105 104 ex Fun M Sat E N u M Sat E N M Sat E N 1 st u = 2 nd u
106 fveqeq2 1 st u = 1 st s M Sat E N 1 st u = 2 nd u M Sat E N 1 st s = 2 nd u
107 eqtr2 M Sat E N 1 st s = 2 nd u M Sat E N 1 st s = 2 nd s 2 nd u = 2 nd s
108 opeq1 j = i j k = i k
109 108 sneqd j = i j k = i k
110 sneq j = i j = i
111 110 difeq2d j = i ω j = ω i
112 111 reseq2d j = i f ω j = f ω i
113 109 112 uneq12d j = i j k f ω j = i k f ω i
114 113 eqcoms i = j j k f ω j = i k f ω i
115 114 adantl 2 nd u = 2 nd s i = j j k f ω j = i k f ω i
116 simpl 2 nd u = 2 nd s i = j 2 nd u = 2 nd s
117 116 eqcomd 2 nd u = 2 nd s i = j 2 nd s = 2 nd u
118 115 117 eleq12d 2 nd u = 2 nd s i = j j k f ω j 2 nd s i k f ω i 2 nd u
119 118 ralbidv 2 nd u = 2 nd s i = j k M j k f ω j 2 nd s k M i k f ω i 2 nd u
120 119 rabbidv 2 nd u = 2 nd s i = j f M ω | k M j k f ω j 2 nd s = f M ω | k M i k f ω i 2 nd u
121 eqeq12 y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z f M ω | k M j k f ω j 2 nd s = f M ω | k M i k f ω i 2 nd u
122 120 121 syl5ibrcom 2 nd u = 2 nd s i = j y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
123 122 exp4b 2 nd u = 2 nd s i = j y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
124 107 123 syl M Sat E N 1 st s = 2 nd u M Sat E N 1 st s = 2 nd s i = j y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
125 124 ex M Sat E N 1 st s = 2 nd u M Sat E N 1 st s = 2 nd s i = j y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
126 106 125 syl6bi 1 st u = 1 st s M Sat E N 1 st u = 2 nd u M Sat E N 1 st s = 2 nd s i = j y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
127 126 com24 1 st u = 1 st s i = j M Sat E N 1 st s = 2 nd s M Sat E N 1 st u = 2 nd u y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
128 127 impcom i = j 1 st u = 1 st s M Sat E N 1 st s = 2 nd s M Sat E N 1 st u = 2 nd u y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
129 128 com13 M Sat E N 1 st u = 2 nd u M Sat E N 1 st s = 2 nd s i = j 1 st u = 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
130 105 129 syl6 Fun M Sat E N u M Sat E N M Sat E N 1 st s = 2 nd s i = j 1 st u = 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
131 130 com23 Fun M Sat E N M Sat E N 1 st s = 2 nd s u M Sat E N i = j 1 st u = 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
132 103 131 syld Fun M Sat E N s M Sat E N u M Sat E N i = j 1 st u = 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
133 132 imp Fun M Sat E N s M Sat E N u M Sat E N i = j 1 st u = 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
134 133 adantr Fun M Sat E N s M Sat E N j ω u M Sat E N i = j 1 st u = 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
135 134 imp Fun M Sat E N s M Sat E N j ω u M Sat E N i = j 1 st u = 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
136 135 adantld Fun M Sat E N s M Sat E N j ω u M Sat E N 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
137 136 ad2antrr Fun M Sat E N s M Sat E N j ω u M Sat E N i ω x = 𝑔 i 1 st u 2 𝑜 = 2 𝑜 i = j 1 st u = 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
138 101 137 sylbid Fun M Sat E N s M Sat E N j ω u M Sat E N i ω x = 𝑔 i 1 st u x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
139 138 impd Fun M Sat E N s M Sat E N j ω u M Sat E N i ω x = 𝑔 i 1 st u x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
140 139 ex Fun M Sat E N s M Sat E N j ω u M Sat E N i ω x = 𝑔 i 1 st u x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s z = f M ω | k M i k f ω i 2 nd u y = z
141 140 com34 Fun M Sat E N s M Sat E N j ω u M Sat E N i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s y = z
142 141 impd Fun M Sat E N s M Sat E N j ω u M Sat E N i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s y = z
143 142 rexlimdva Fun M Sat E N s M Sat E N j ω u M Sat E N i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s y = z
144 92 143 jaod Fun M Sat E N s M Sat E N j ω u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s y = z
145 144 rexlimdva Fun M Sat E N s M Sat E N j ω u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s y = z
146 145 com23 Fun M Sat E N s M Sat E N j ω x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
147 146 rexlimdva Fun M Sat E N s M Sat E N j ω x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
148 70 147 jaod Fun M Sat E N s M Sat E N r M Sat E N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
149 148 rexlimdva Fun M Sat E N s M Sat E N r M Sat E N x = 1 st s 𝑔 1 st r y = M ω 2 nd s 2 nd r j ω x = 𝑔 j 1 st s y = f M ω | k M j k f ω j 2 nd s u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
150 31 149 syl5bi Fun M Sat E N u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
151 150 impd Fun M Sat E N u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
152 151 alrimivv Fun M Sat E N y z u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
153 eqeq1 y = z y = M ω 2 nd u 2 nd v z = M ω 2 nd u 2 nd v
154 153 anbi2d y = z x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v
155 154 rexbidv y = z v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v
156 eqeq1 y = z y = f M ω | k M i k f ω i 2 nd u z = f M ω | k M i k f ω i 2 nd u
157 156 anbi2d y = z x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u
158 157 rexbidv y = z i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u
159 155 158 orbi12d y = z v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u
160 159 rexbidv y = z u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u
161 160 mo4 * y u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u y z u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v z = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u z = f M ω | k M i k f ω i 2 nd u y = z
162 152 161 sylibr Fun M Sat E N * y u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u
163 162 alrimiv Fun M Sat E N x * y u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u
164 funopab Fun x y | u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u x * y u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u
165 163 164 sylibr Fun M Sat E N Fun x y | u M Sat E N v M Sat E N x = 1 st u 𝑔 1 st v y = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u y = f M ω | k M i k f ω i 2 nd u