Metamath Proof Explorer

Theorem satffunlem1lem2

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

Ref Expression
Assertion satffunlem1lem2 
|- ( ( M e. V /\ E e. W ) -> ( dom ( ( M Sat E ) ` (/) ) i^i dom { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) = (/) )

Proof

Step Hyp Ref Expression
1 peano1 
 |-  (/) e. _om
2 satfdmfmla 
 |-  ( ( M e. V /\ E e. W /\ (/) e. _om ) -> dom ( ( M Sat E ) ` (/) ) = ( Fmla ` (/) ) )
3 1 2 mp3an3 
 |-  ( ( M e. V /\ E e. W ) -> dom ( ( M Sat E ) ` (/) ) = ( Fmla ` (/) ) )
4 ovex 
 |-  ( M ^m _om ) e. _V
5 4 difexi 
 |-  ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. _V
6 5 a1i 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ v e. ( ( M Sat E ) ` (/) ) ) -> ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. _V )
7 6 ralrimiva 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> A. v e. ( ( M Sat E ) ` (/) ) ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. _V )
8 4 rabex 
 |-  { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. _V
9 8 a1i 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ i e. _om ) -> { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. _V )
10 9 ralrimiva 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> A. i e. _om { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. _V )
11 7 10 jca 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( A. v e. ( ( M Sat E ) ` (/) ) ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. _V /\ A. i e. _om { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. _V ) )
12 11 ralrimiva 
 |-  ( ( M e. V /\ E e. W ) -> A. u e. ( ( M Sat E ) ` (/) ) ( A. v e. ( ( M Sat E ) ` (/) ) ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. _V /\ A. i e. _om { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. _V ) )
13 dmopab2rex 
 |-  ( A. u e. ( ( M Sat E ) ` (/) ) ( A. v e. ( ( M Sat E ) ` (/) ) ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. _V /\ A. i e. _om { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. _V ) -> dom { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } = { x | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } )
14 12 13 syl 
 |-  ( ( M e. V /\ E e. W ) -> dom { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } = { x | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } )
15 satfrel 
 |-  ( ( M e. V /\ E e. W /\ (/) e. _om ) -> Rel ( ( M Sat E ) ` (/) ) )
16 1 15 mp3an3 
 |-  ( ( M e. V /\ E e. W ) -> Rel ( ( M Sat E ) ` (/) ) )
17 1stdm 
 |-  ( ( Rel ( ( M Sat E ) ` (/) ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( 1st ` u ) e. dom ( ( M Sat E ) ` (/) ) )
18 16 17 sylan 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( 1st ` u ) e. dom ( ( M Sat E ) ` (/) ) )
19 2 eqcomd 
 |-  ( ( M e. V /\ E e. W /\ (/) e. _om ) -> ( Fmla ` (/) ) = dom ( ( M Sat E ) ` (/) ) )
20 1 19 mp3an3 
 |-  ( ( M e. V /\ E e. W ) -> ( Fmla ` (/) ) = dom ( ( M Sat E ) ` (/) ) )
21 20 adantr 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( Fmla ` (/) ) = dom ( ( M Sat E ) ` (/) ) )
22 18 21 eleqtrrd 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( 1st ` u ) e. ( Fmla ` (/) ) )
23 22 adantr 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) -> ( 1st ` u ) e. ( Fmla ` (/) ) )
24 oveq1 
 |-  ( f = ( 1st ` u ) -> ( f |g g ) = ( ( 1st ` u ) |g g ) )
25 24 eqeq2d 
 |-  ( f = ( 1st ` u ) -> ( x = ( f |g g ) <-> x = ( ( 1st ` u ) |g g ) ) )
26 25 rexbidv 
 |-  ( f = ( 1st ` u ) -> ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) <-> E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) ) )
27 eqidd 
 |-  ( f = ( 1st ` u ) -> i = i )
28 id 
 |-  ( f = ( 1st ` u ) -> f = ( 1st ` u ) )
29 27 28 goaleq12d 
 |-  ( f = ( 1st ` u ) -> A.g i f = A.g i ( 1st ` u ) )
30 29 eqeq2d 
 |-  ( f = ( 1st ` u ) -> ( x = A.g i f <-> x = A.g i ( 1st ` u ) ) )
31 30 rexbidv 
 |-  ( f = ( 1st ` u ) -> ( E. i e. _om x = A.g i f <-> E. i e. _om x = A.g i ( 1st ` u ) ) )
32 26 31 orbi12d 
 |-  ( f = ( 1st ` u ) -> ( ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) <-> ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
33 32 adantl 
 |-  ( ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) /\ f = ( 1st ` u ) ) -> ( ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) <-> ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
34 1stdm 
 |-  ( ( Rel ( ( M Sat E ) ` (/) ) /\ v e. ( ( M Sat E ) ` (/) ) ) -> ( 1st ` v ) e. dom ( ( M Sat E ) ` (/) ) )
35 16 34 sylan 
 |-  ( ( ( M e. V /\ E e. W ) /\ v e. ( ( M Sat E ) ` (/) ) ) -> ( 1st ` v ) e. dom ( ( M Sat E ) ` (/) ) )
36 20 adantr 
 |-  ( ( ( M e. V /\ E e. W ) /\ v e. ( ( M Sat E ) ` (/) ) ) -> ( Fmla ` (/) ) = dom ( ( M Sat E ) ` (/) ) )
37 35 36 eleqtrrd 
 |-  ( ( ( M e. V /\ E e. W ) /\ v e. ( ( M Sat E ) ` (/) ) ) -> ( 1st ` v ) e. ( Fmla ` (/) ) )
38 37 ad4ant13 
 |-  ( ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ v e. ( ( M Sat E ) ` (/) ) ) /\ x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) -> ( 1st ` v ) e. ( Fmla ` (/) ) )
39 oveq2 
 |-  ( g = ( 1st ` v ) -> ( ( 1st ` u ) |g g ) = ( ( 1st ` u ) |g ( 1st ` v ) ) )
40 39 eqeq2d 
 |-  ( g = ( 1st ` v ) -> ( x = ( ( 1st ` u ) |g g ) <-> x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
41 40 adantl 
 |-  ( ( ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ v e. ( ( M Sat E ) ` (/) ) ) /\ x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) /\ g = ( 1st ` v ) ) -> ( x = ( ( 1st ` u ) |g g ) <-> x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
42 simpr 
 |-  ( ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ v e. ( ( M Sat E ) ` (/) ) ) /\ x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) -> x = ( ( 1st ` u ) |g ( 1st ` v ) ) )
43 38 41 42 rspcedvd 
 |-  ( ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ v e. ( ( M Sat E ) ` (/) ) ) /\ x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) -> E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) )
44 43 ex 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ v e. ( ( M Sat E ) ` (/) ) ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) ) )
45 44 rexlimdva 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) ) )
46 45 orim1d 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) -> ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
47 46 imp 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) -> ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) )
48 23 33 47 rspcedvd 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) -> E. f e. ( Fmla ` (/) ) ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) )
49 48 ex 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) -> E. f e. ( Fmla ` (/) ) ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) )
50 49 rexlimdva 
 |-  ( ( M e. V /\ E e. W ) -> ( E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) -> E. f e. ( Fmla ` (/) ) ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) )
51 releldm2 
 |-  ( Rel ( ( M Sat E ) ` (/) ) -> ( f e. dom ( ( M Sat E ) ` (/) ) <-> E. u e. ( ( M Sat E ) ` (/) ) ( 1st ` u ) = f ) )
52 16 51 syl 
 |-  ( ( M e. V /\ E e. W ) -> ( f e. dom ( ( M Sat E ) ` (/) ) <-> E. u e. ( ( M Sat E ) ` (/) ) ( 1st ` u ) = f ) )
53 3 eleq2d 
 |-  ( ( M e. V /\ E e. W ) -> ( f e. dom ( ( M Sat E ) ` (/) ) <-> f e. ( Fmla ` (/) ) ) )
54 52 53 bitr3d 
 |-  ( ( M e. V /\ E e. W ) -> ( E. u e. ( ( M Sat E ) ` (/) ) ( 1st ` u ) = f <-> f e. ( Fmla ` (/) ) ) )
55 r19.41v 
 |-  ( E. u e. ( ( M Sat E ) ` (/) ) ( ( 1st ` u ) = f /\ ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) <-> ( E. u e. ( ( M Sat E ) ` (/) ) ( 1st ` u ) = f /\ ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) )
56 oveq1 
 |-  ( ( 1st ` u ) = f -> ( ( 1st ` u ) |g g ) = ( f |g g ) )
57 56 eqeq2d 
 |-  ( ( 1st ` u ) = f -> ( x = ( ( 1st ` u ) |g g ) <-> x = ( f |g g ) ) )
58 57 rexbidv 
 |-  ( ( 1st ` u ) = f -> ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) <-> E. g e. ( Fmla ` (/) ) x = ( f |g g ) ) )
59 eqidd 
 |-  ( ( 1st ` u ) = f -> i = i )
60 id 
 |-  ( ( 1st ` u ) = f -> ( 1st ` u ) = f )
61 59 60 goaleq12d 
 |-  ( ( 1st ` u ) = f -> A.g i ( 1st ` u ) = A.g i f )
62 61 eqeq2d 
 |-  ( ( 1st ` u ) = f -> ( x = A.g i ( 1st ` u ) <-> x = A.g i f ) )
63 62 rexbidv 
 |-  ( ( 1st ` u ) = f -> ( E. i e. _om x = A.g i ( 1st ` u ) <-> E. i e. _om x = A.g i f ) )
64 58 63 orbi12d 
 |-  ( ( 1st ` u ) = f -> ( ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) )
65 64 adantl 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ ( 1st ` u ) = f ) -> ( ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) )
66 3 eqcomd 
 |-  ( ( M e. V /\ E e. W ) -> ( Fmla ` (/) ) = dom ( ( M Sat E ) ` (/) ) )
67 66 eleq2d 
 |-  ( ( M e. V /\ E e. W ) -> ( g e. ( Fmla ` (/) ) <-> g e. dom ( ( M Sat E ) ` (/) ) ) )
68 releldm2 
 |-  ( Rel ( ( M Sat E ) ` (/) ) -> ( g e. dom ( ( M Sat E ) ` (/) ) <-> E. v e. ( ( M Sat E ) ` (/) ) ( 1st ` v ) = g ) )
69 16 68 syl 
 |-  ( ( M e. V /\ E e. W ) -> ( g e. dom ( ( M Sat E ) ` (/) ) <-> E. v e. ( ( M Sat E ) ` (/) ) ( 1st ` v ) = g ) )
70 67 69 bitrd 
 |-  ( ( M e. V /\ E e. W ) -> ( g e. ( Fmla ` (/) ) <-> E. v e. ( ( M Sat E ) ` (/) ) ( 1st ` v ) = g ) )
71 r19.41v 
 |-  ( E. v e. ( ( M Sat E ) ` (/) ) ( ( 1st ` v ) = g /\ x = ( ( 1st ` u ) |g g ) ) <-> ( E. v e. ( ( M Sat E ) ` (/) ) ( 1st ` v ) = g /\ x = ( ( 1st ` u ) |g g ) ) )
72 39 eqcoms 
 |-  ( ( 1st ` v ) = g -> ( ( 1st ` u ) |g g ) = ( ( 1st ` u ) |g ( 1st ` v ) ) )
73 72 eqeq2d 
 |-  ( ( 1st ` v ) = g -> ( x = ( ( 1st ` u ) |g g ) <-> x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
74 73 biimpa 
 |-  ( ( ( 1st ` v ) = g /\ x = ( ( 1st ` u ) |g g ) ) -> x = ( ( 1st ` u ) |g ( 1st ` v ) ) )
75 74 a1i 
 |-  ( ( M e. V /\ E e. W ) -> ( ( ( 1st ` v ) = g /\ x = ( ( 1st ` u ) |g g ) ) -> x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
76 75 reximdv 
 |-  ( ( M e. V /\ E e. W ) -> ( E. v e. ( ( M Sat E ) ` (/) ) ( ( 1st ` v ) = g /\ x = ( ( 1st ` u ) |g g ) ) -> E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
77 71 76 biimtrrid 
 |-  ( ( M e. V /\ E e. W ) -> ( ( E. v e. ( ( M Sat E ) ` (/) ) ( 1st ` v ) = g /\ x = ( ( 1st ` u ) |g g ) ) -> E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
78 77 expd 
 |-  ( ( M e. V /\ E e. W ) -> ( E. v e. ( ( M Sat E ) ` (/) ) ( 1st ` v ) = g -> ( x = ( ( 1st ` u ) |g g ) -> E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) ) )
79 70 78 sylbid 
 |-  ( ( M e. V /\ E e. W ) -> ( g e. ( Fmla ` (/) ) -> ( x = ( ( 1st ` u ) |g g ) -> E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) ) )
80 79 rexlimdv 
 |-  ( ( M e. V /\ E e. W ) -> ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) -> E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
81 80 adantr 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) -> E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
82 81 adantr 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ ( 1st ` u ) = f ) -> ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) -> E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
83 82 orim1d 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ ( 1st ` u ) = f ) -> ( ( E. g e. ( Fmla ` (/) ) x = ( ( 1st ` u ) |g g ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) -> ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
84 65 83 sylbird 
 |-  ( ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) /\ ( 1st ` u ) = f ) -> ( ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) -> ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
85 84 expimpd 
 |-  ( ( ( M e. V /\ E e. W ) /\ u e. ( ( M Sat E ) ` (/) ) ) -> ( ( ( 1st ` u ) = f /\ ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) -> ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
86 85 reximdva 
 |-  ( ( M e. V /\ E e. W ) -> ( E. u e. ( ( M Sat E ) ` (/) ) ( ( 1st ` u ) = f /\ ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) -> E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
87 55 86 biimtrrid 
 |-  ( ( M e. V /\ E e. W ) -> ( ( E. u e. ( ( M Sat E ) ` (/) ) ( 1st ` u ) = f /\ ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) -> E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
88 87 expd 
 |-  ( ( M e. V /\ E e. W ) -> ( E. u e. ( ( M Sat E ) ` (/) ) ( 1st ` u ) = f -> ( ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) -> E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) )
89 54 88 sylbird 
 |-  ( ( M e. V /\ E e. W ) -> ( f e. ( Fmla ` (/) ) -> ( ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) -> E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) )
90 89 rexlimdv 
 |-  ( ( M e. V /\ E e. W ) -> ( E. f e. ( Fmla ` (/) ) ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) -> E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
91 50 90 impbid 
 |-  ( ( M e. V /\ E e. W ) -> ( E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> E. f e. ( Fmla ` (/) ) ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) ) )
92 91 abbidv 
 |-  ( ( M e. V /\ E e. W ) -> { x | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } = { x | E. f e. ( Fmla ` (/) ) ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) } )
93 14 92 eqtrd 
 |-  ( ( M e. V /\ E e. W ) -> dom { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } = { x | E. f e. ( Fmla ` (/) ) ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) } )
94 3 93 ineq12d 
 |-  ( ( M e. V /\ E e. W ) -> ( dom ( ( M Sat E ) ` (/) ) i^i dom { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) = ( ( Fmla ` (/) ) i^i { x | E. f e. ( Fmla ` (/) ) ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) } ) )
95 fmla0disjsuc 
 |-  ( ( Fmla ` (/) ) i^i { x | E. f e. ( Fmla ` (/) ) ( E. g e. ( Fmla ` (/) ) x = ( f |g g ) \/ E. i e. _om x = A.g i f ) } ) = (/)
96 94 95 eqtrdi 
 |-  ( ( M e. V /\ E e. W ) -> ( dom ( ( M Sat E ) ` (/) ) i^i dom { <. x , y >. | E. u e. ( ( M Sat E ) ` (/) ) ( E. v e. ( ( M Sat E ) ` (/) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { f e. ( M ^m _om ) | A. j e. M ( { <. i , j >. } u. ( f |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) = (/) )