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