Metamath Proof Explorer


Theorem satfdm

Description: The domain of the satisfaction predicate as function over wff codes does not depend on the model M and the binary relation E on M . (Contributed by AV, 13-Oct-2023)

Ref Expression
Assertion satfdm M V E W N X F Y n ω dom M Sat E n = dom N Sat F n

Proof

Step Hyp Ref Expression
1 fveq2 x = M Sat E x = M Sat E
2 1 dmeqd x = dom M Sat E x = dom M Sat E
3 fveq2 x = N Sat F x = N Sat F
4 3 dmeqd x = dom N Sat F x = dom N Sat F
5 2 4 eqeq12d x = dom M Sat E x = dom N Sat F x dom M Sat E = dom N Sat F
6 5 imbi2d x = M V E W N X F Y dom M Sat E x = dom N Sat F x M V E W N X F Y dom M Sat E = dom N Sat F
7 fveq2 x = y M Sat E x = M Sat E y
8 7 dmeqd x = y dom M Sat E x = dom M Sat E y
9 fveq2 x = y N Sat F x = N Sat F y
10 9 dmeqd x = y dom N Sat F x = dom N Sat F y
11 8 10 eqeq12d x = y dom M Sat E x = dom N Sat F x dom M Sat E y = dom N Sat F y
12 11 imbi2d x = y M V E W N X F Y dom M Sat E x = dom N Sat F x M V E W N X F Y dom M Sat E y = dom N Sat F y
13 fveq2 x = suc y M Sat E x = M Sat E suc y
14 13 dmeqd x = suc y dom M Sat E x = dom M Sat E suc y
15 fveq2 x = suc y N Sat F x = N Sat F suc y
16 15 dmeqd x = suc y dom N Sat F x = dom N Sat F suc y
17 14 16 eqeq12d x = suc y dom M Sat E x = dom N Sat F x dom M Sat E suc y = dom N Sat F suc y
18 17 imbi2d x = suc y M V E W N X F Y dom M Sat E x = dom N Sat F x M V E W N X F Y dom M Sat E suc y = dom N Sat F suc y
19 fveq2 x = n M Sat E x = M Sat E n
20 19 dmeqd x = n dom M Sat E x = dom M Sat E n
21 fveq2 x = n N Sat F x = N Sat F n
22 21 dmeqd x = n dom N Sat F x = dom N Sat F n
23 20 22 eqeq12d x = n dom M Sat E x = dom N Sat F x dom M Sat E n = dom N Sat F n
24 23 imbi2d x = n M V E W N X F Y dom M Sat E x = dom N Sat F x M V E W N X F Y dom M Sat E n = dom N Sat F n
25 rexcom4 v ω y x = u 𝑔 v y = a M ω | a u E a v y v ω x = u 𝑔 v y = a M ω | a u E a v
26 25 rexbii u ω v ω y x = u 𝑔 v y = a M ω | a u E a v u ω y v ω x = u 𝑔 v y = a M ω | a u E a v
27 ovex M ω V
28 27 rabex a M ω | a u E a v V
29 28 isseti y y = a M ω | a u E a v
30 ovex N ω V
31 30 rabex a N ω | a u F a v V
32 31 isseti z z = a N ω | a u F a v
33 29 32 2th y y = a M ω | a u E a v z z = a N ω | a u F a v
34 33 anbi2i x = u 𝑔 v y y = a M ω | a u E a v x = u 𝑔 v z z = a N ω | a u F a v
35 19.42v y x = u 𝑔 v y = a M ω | a u E a v x = u 𝑔 v y y = a M ω | a u E a v
36 19.42v z x = u 𝑔 v z = a N ω | a u F a v x = u 𝑔 v z z = a N ω | a u F a v
37 34 35 36 3bitr4i y x = u 𝑔 v y = a M ω | a u E a v z x = u 𝑔 v z = a N ω | a u F a v
38 37 rexbii v ω y x = u 𝑔 v y = a M ω | a u E a v v ω z x = u 𝑔 v z = a N ω | a u F a v
39 38 rexbii u ω v ω y x = u 𝑔 v y = a M ω | a u E a v u ω v ω z x = u 𝑔 v z = a N ω | a u F a v
40 rexcom4 u ω y v ω x = u 𝑔 v y = a M ω | a u E a v y u ω v ω x = u 𝑔 v y = a M ω | a u E a v
41 26 39 40 3bitr3ri y u ω v ω x = u 𝑔 v y = a M ω | a u E a v u ω v ω z x = u 𝑔 v z = a N ω | a u F a v
42 rexcom4 v ω z x = u 𝑔 v z = a N ω | a u F a v z v ω x = u 𝑔 v z = a N ω | a u F a v
43 42 rexbii u ω v ω z x = u 𝑔 v z = a N ω | a u F a v u ω z v ω x = u 𝑔 v z = a N ω | a u F a v
44 41 43 bitri y u ω v ω x = u 𝑔 v y = a M ω | a u E a v u ω z v ω x = u 𝑔 v z = a N ω | a u F a v
45 rexcom4 u ω z v ω x = u 𝑔 v z = a N ω | a u F a v z u ω v ω x = u 𝑔 v z = a N ω | a u F a v
46 44 45 bitri y u ω v ω x = u 𝑔 v y = a M ω | a u E a v z u ω v ω x = u 𝑔 v z = a N ω | a u F a v
47 46 abbii x | y u ω v ω x = u 𝑔 v y = a M ω | a u E a v = x | z u ω v ω x = u 𝑔 v z = a N ω | a u F a v
48 eqid M Sat E = M Sat E
49 48 satfv0 M V E W M Sat E = x y | u ω v ω x = u 𝑔 v y = a M ω | a u E a v
50 49 dmeqd M V E W dom M Sat E = dom x y | u ω v ω x = u 𝑔 v y = a M ω | a u E a v
51 dmopab dom x y | u ω v ω x = u 𝑔 v y = a M ω | a u E a v = x | y u ω v ω x = u 𝑔 v y = a M ω | a u E a v
52 50 51 eqtrdi M V E W dom M Sat E = x | y u ω v ω x = u 𝑔 v y = a M ω | a u E a v
53 52 adantr M V E W N X F Y dom M Sat E = x | y u ω v ω x = u 𝑔 v y = a M ω | a u E a v
54 eqid N Sat F = N Sat F
55 54 satfv0 N X F Y N Sat F = x z | u ω v ω x = u 𝑔 v z = a N ω | a u F a v
56 55 dmeqd N X F Y dom N Sat F = dom x z | u ω v ω x = u 𝑔 v z = a N ω | a u F a v
57 dmopab dom x z | u ω v ω x = u 𝑔 v z = a N ω | a u F a v = x | z u ω v ω x = u 𝑔 v z = a N ω | a u F a v
58 56 57 eqtrdi N X F Y dom N Sat F = x | z u ω v ω x = u 𝑔 v z = a N ω | a u F a v
59 58 adantl M V E W N X F Y dom N Sat F = x | z u ω v ω x = u 𝑔 v z = a N ω | a u F a v
60 47 53 59 3eqtr4a M V E W N X F Y dom M Sat E = dom N Sat F
61 pm2.27 M V E W N X F Y M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E y = dom N Sat F y
62 61 adantl y ω M V E W N X F Y M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E y = dom N Sat F y
63 simpr y ω M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E y = dom N Sat F y
64 simprl y ω M V E W N X F Y M V E W
65 simpl y ω M V E W N X F Y y ω
66 df-3an M V E W y ω M V E W y ω
67 64 65 66 sylanbrc y ω M V E W N X F Y M V E W y ω
68 satfdmlem M V E W y ω dom M Sat E y = dom N Sat F y u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
69 67 68 sylan y ω M V E W N X F Y dom M Sat E y = dom N Sat F y u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
70 simprr y ω M V E W N X F Y N X F Y
71 df-3an N X F Y y ω N X F Y y ω
72 70 65 71 sylanbrc y ω M V E W N X F Y N X F Y y ω
73 id dom M Sat E y = dom N Sat F y dom M Sat E y = dom N Sat F y
74 73 eqcomd dom M Sat E y = dom N Sat F y dom N Sat F y = dom M Sat E y
75 satfdmlem N X F Y y ω dom N Sat F y = dom M Sat E y a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
76 72 74 75 syl2an y ω M V E W N X F Y dom M Sat E y = dom N Sat F y a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
77 69 76 impbid y ω M V E W N X F Y dom M Sat E y = dom N Sat F y u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
78 27 difexi M ω 2 nd u 2 nd v V
79 78 isseti w w = M ω 2 nd u 2 nd v
80 79 biantru x = 1 st u 𝑔 1 st v x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v
81 80 bicomi x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v x = 1 st u 𝑔 1 st v
82 81 rexbii v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v v M Sat E y x = 1 st u 𝑔 1 st v
83 27 rabex m M ω | f M i f m ω i 2 nd u V
84 83 isseti w w = m M ω | f M i f m ω i 2 nd u
85 84 biantru x = 𝑔 i 1 st u x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u
86 85 bicomi x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u x = 𝑔 i 1 st u
87 86 rexbii i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u i ω x = 𝑔 i 1 st u
88 82 87 orbi12i v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u v M Sat E y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
89 88 rexbii u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v i ω x = 𝑔 i 1 st u
90 30 difexi N ω 2 nd a 2 nd b V
91 90 isseti z z = N ω 2 nd a 2 nd b
92 91 biantru x = 1 st a 𝑔 1 st b x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b
93 92 bicomi x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b x = 1 st a 𝑔 1 st b
94 93 rexbii b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b b N Sat F y x = 1 st a 𝑔 1 st b
95 30 rabex m N ω | f N i f m ω i 2 nd a V
96 95 isseti z z = m N ω | f N i f m ω i 2 nd a
97 96 biantru x = 𝑔 i 1 st a x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a
98 97 bicomi x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a x = 𝑔 i 1 st a
99 98 rexbii i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a i ω x = 𝑔 i 1 st a
100 94 99 orbi12i b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a b N Sat F y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
101 100 rexbii a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b i ω x = 𝑔 i 1 st a
102 77 89 101 3bitr4g y ω M V E W N X F Y dom M Sat E y = dom N Sat F y u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a
103 19.42v w x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v
104 103 bicomi x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v w x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v
105 104 rexbii v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v v M Sat E y w x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v
106 rexcom4 v M Sat E y w x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v
107 105 106 bitri v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v
108 19.42v w x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u
109 108 bicomi x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u w x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
110 109 rexbii i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u i ω w x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
111 rexcom4 i ω w x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u w i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
112 110 111 bitri i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u w i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
113 107 112 orbi12i v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v w i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
114 19.43 w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v w i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
115 114 bicomi w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v w i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
116 113 115 bitri v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
117 116 rexbii u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u u M Sat E y w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
118 rexcom4 u M Sat E y w v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u w u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
119 117 118 bitri u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w w = m M ω | f M i f m ω i 2 nd u w u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
120 19.42v z x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b
121 120 bicomi x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b z x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b
122 121 rexbii b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b b N Sat F y z x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b
123 rexcom4 b N Sat F y z x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b
124 122 123 bitri b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b
125 19.42v z x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a
126 125 bicomi x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a z x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
127 126 rexbii i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a i ω z x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
128 rexcom4 i ω z x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a z i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
129 127 128 bitri i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a z i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
130 124 129 orbi12i b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b z i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
131 19.43 z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b z i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
132 131 bicomi z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b z i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
133 130 132 bitri b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
134 133 rexbii a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a a N Sat F y z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
135 rexcom4 a N Sat F y z b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a z a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
136 134 135 bitri a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z z = m N ω | f N i f m ω i 2 nd a z a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
137 102 119 136 3bitr3g y ω M V E W N X F Y dom M Sat E y = dom N Sat F y w u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u z a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
138 137 abbidv y ω M V E W N X F Y dom M Sat E y = dom N Sat F y x | w u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u = x | z a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
139 dmopab dom x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u = x | w u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
140 dmopab dom x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a = x | z a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
141 138 139 140 3eqtr4g y ω M V E W N X F Y dom M Sat E y = dom N Sat F y dom x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u = dom x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
142 63 141 uneq12d y ω M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E y dom x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u = dom N Sat F y dom x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
143 dmun dom M Sat E y x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u = dom M Sat E y dom x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
144 dmun dom N Sat F y x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a = dom N Sat F y dom x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
145 142 143 144 3eqtr4g y ω M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E y x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u = dom N Sat F y x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
146 simpl M V E W M V
147 146 adantr M V E W N X F Y M V
148 simpr M V E W E W
149 148 adantr M V E W N X F Y E W
150 48 satfvsuc M V E W y ω M Sat E suc y = M Sat E y x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
151 147 149 65 150 syl2an23an y ω M V E W N X F Y M Sat E suc y = M Sat E y x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
152 151 dmeqd y ω M V E W N X F Y dom M Sat E suc y = dom M Sat E y x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u
153 simprl M V E W N X F Y N X
154 simprr M V E W N X F Y F Y
155 54 satfvsuc N X F Y y ω N Sat F suc y = N Sat F y x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
156 153 154 65 155 syl2an23an y ω M V E W N X F Y N Sat F suc y = N Sat F y x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
157 156 dmeqd y ω M V E W N X F Y dom N Sat F suc y = dom N Sat F y x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
158 152 157 eqeq12d y ω M V E W N X F Y dom M Sat E suc y = dom N Sat F suc y dom M Sat E y x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u = dom N Sat F y x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
159 158 adantr y ω M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E suc y = dom N Sat F suc y dom M Sat E y x w | u M Sat E y v M Sat E y x = 1 st u 𝑔 1 st v w = M ω 2 nd u 2 nd v i ω x = 𝑔 i 1 st u w = m M ω | f M i f m ω i 2 nd u = dom N Sat F y x z | a N Sat F y b N Sat F y x = 1 st a 𝑔 1 st b z = N ω 2 nd a 2 nd b i ω x = 𝑔 i 1 st a z = m N ω | f N i f m ω i 2 nd a
160 145 159 mpbird y ω M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E suc y = dom N Sat F suc y
161 160 ex y ω M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E suc y = dom N Sat F suc y
162 62 161 syld y ω M V E W N X F Y M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E suc y = dom N Sat F suc y
163 162 ex y ω M V E W N X F Y M V E W N X F Y dom M Sat E y = dom N Sat F y dom M Sat E suc y = dom N Sat F suc y
164 163 com23 y ω M V E W N X F Y dom M Sat E y = dom N Sat F y M V E W N X F Y dom M Sat E suc y = dom N Sat F suc y
165 6 12 18 24 60 164 finds n ω M V E W N X F Y dom M Sat E n = dom N Sat F n
166 165 impcom M V E W N X F Y n ω dom M Sat E n = dom N Sat F n
167 166 ralrimiva M V E W N X F Y n ω dom M Sat E n = dom N Sat F n