Metamath Proof Explorer

Theorem satffunlem2lem2

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

Ref Expression
Hypotheses satffunlem2lem2.s 
|- S = ( M Sat E )
satffunlem2lem2.a 
|- A = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) )
satffunlem2lem2.b 
|- B = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) }
Assertion satffunlem2lem2 
|- ( ( ( N e. _om /\ ( M e. V /\ E e. W ) ) /\ Fun ( S ` suc N ) ) -> ( dom ( S ` suc N ) i^i dom { <. x , y >. | ( E. u e. ( ( S ` suc N ) \ ( S ` N ) ) ( E. v e. ( S ` suc N ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = B ) ) \/ E. u e. ( S ` N ) E. v e. ( ( S ` suc N ) \ ( S ` N ) ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = A ) ) } ) = (/) )

Proof

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