Metamath Proof Explorer

Theorem satfdmlem

Description: Lemma for satfdm . (Contributed by AV, 12-Oct-2023)

Ref Expression
Assertion 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 ) ) ) )

Proof

Step Hyp Ref Expression
1 satfrel 
 |-  ( ( M e. V /\ E e. W /\ Y e. _om ) -> Rel ( ( M Sat E ) ` Y ) )
2 1 adantr 
 |-  ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) -> Rel ( ( M Sat E ) ` Y ) )
3 1stdm 
 |-  ( ( Rel ( ( M Sat E ) ` Y ) /\ u e. ( ( M Sat E ) ` Y ) ) -> ( 1st ` u ) e. dom ( ( M Sat E ) ` Y ) )
4 2 3 sylan 
 |-  ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) -> ( 1st ` u ) e. dom ( ( M Sat E ) ` Y ) )
5 eleq2 
 |-  ( dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) -> ( ( 1st ` u ) e. dom ( ( M Sat E ) ` Y ) <-> ( 1st ` u ) e. dom ( ( N Sat F ) ` Y ) ) )
6 5 adantl 
 |-  ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) -> ( ( 1st ` u ) e. dom ( ( M Sat E ) ` Y ) <-> ( 1st ` u ) e. dom ( ( N Sat F ) ` Y ) ) )
7 6 adantr 
 |-  ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) -> ( ( 1st ` u ) e. dom ( ( M Sat E ) ` Y ) <-> ( 1st ` u ) e. dom ( ( N Sat F ) ` Y ) ) )
8 fvex 
 |-  ( 1st ` u ) e. _V
9 eldm2g 
 |-  ( ( 1st ` u ) e. _V -> ( ( 1st ` u ) e. dom ( ( N Sat F ) ` Y ) <-> E. s <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) )
10 8 9 ax-mp 
 |-  ( ( 1st ` u ) e. dom ( ( N Sat F ) ` Y ) <-> E. s <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) )
11 simpr 
 |-  ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) -> <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) )
12 2 ad4antr 
 |-  ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) -> Rel ( ( M Sat E ) ` Y ) )
13 1stdm 
 |-  ( ( Rel ( ( M Sat E ) ` Y ) /\ v e. ( ( M Sat E ) ` Y ) ) -> ( 1st ` v ) e. dom ( ( M Sat E ) ` Y ) )
14 12 13 sylancom 
 |-  ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) -> ( 1st ` v ) e. dom ( ( M Sat E ) ` Y ) )
15 eleq2 
 |-  ( dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) -> ( ( 1st ` v ) e. dom ( ( M Sat E ) ` Y ) <-> ( 1st ` v ) e. dom ( ( N Sat F ) ` Y ) ) )
16 15 ad5antlr 
 |-  ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) -> ( ( 1st ` v ) e. dom ( ( M Sat E ) ` Y ) <-> ( 1st ` v ) e. dom ( ( N Sat F ) ` Y ) ) )
17 fvex 
 |-  ( 1st ` v ) e. _V
18 eldm2g 
 |-  ( ( 1st ` v ) e. _V -> ( ( 1st ` v ) e. dom ( ( N Sat F ) ` Y ) <-> E. r <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) ) )
19 17 18 ax-mp 
 |-  ( ( 1st ` v ) e. dom ( ( N Sat F ) ` Y ) <-> E. r <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) )
20 simpr 
 |-  ( ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) ) -> <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) )
21 vex 
 |-  s e. _V
22 8 21 op1std 
 |-  ( a = <. ( 1st ` u ) , s >. -> ( 1st ` a ) = ( 1st ` u ) )
23 22 eqcomd 
 |-  ( a = <. ( 1st ` u ) , s >. -> ( 1st ` u ) = ( 1st ` a ) )
24 23 ad3antlr 
 |-  ( ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) ) -> ( 1st ` u ) = ( 1st ` a ) )
25 vex 
 |-  r e. _V
26 17 25 op1std 
 |-  ( b = <. ( 1st ` v ) , r >. -> ( 1st ` b ) = ( 1st ` v ) )
27 26 eqcomd 
 |-  ( b = <. ( 1st ` v ) , r >. -> ( 1st ` v ) = ( 1st ` b ) )
28 24 27 oveqan12d 
 |-  ( ( ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) ) /\ b = <. ( 1st ` v ) , r >. ) -> ( ( 1st ` u ) |g ( 1st ` v ) ) = ( ( 1st ` a ) |g ( 1st ` b ) ) )
29 28 eqeq2d 
 |-  ( ( ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) ) /\ b = <. ( 1st ` v ) , r >. ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> x = ( ( 1st ` a ) |g ( 1st ` b ) ) ) )
30 29 biimpd 
 |-  ( ( ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) ) /\ b = <. ( 1st ` v ) , r >. ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> x = ( ( 1st ` a ) |g ( 1st ` b ) ) ) )
31 20 30 rspcimedv 
 |-  ( ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. b e. ( ( N Sat F ) ` Y ) x = ( ( 1st ` a ) |g ( 1st ` b ) ) ) )
32 31 ex 
 |-  ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) -> ( <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. b e. ( ( N Sat F ) ` Y ) x = ( ( 1st ` a ) |g ( 1st ` b ) ) ) ) )
33 32 exlimdv 
 |-  ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) -> ( E. r <. ( 1st ` v ) , r >. e. ( ( N Sat F ) ` Y ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. b e. ( ( N Sat F ) ` Y ) x = ( ( 1st ` a ) |g ( 1st ` b ) ) ) ) )
34 19 33 syl5bi 
 |-  ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) -> ( ( 1st ` v ) e. dom ( ( N Sat F ) ` Y ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. b e. ( ( N Sat F ) ` Y ) x = ( ( 1st ` a ) |g ( 1st ` b ) ) ) ) )
35 16 34 sylbid 
 |-  ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) -> ( ( 1st ` v ) e. dom ( ( M Sat E ) ` Y ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. b e. ( ( N Sat F ) ` Y ) x = ( ( 1st ` a ) |g ( 1st ` b ) ) ) ) )
36 14 35 mpd 
 |-  ( ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) /\ v e. ( ( M Sat E ) ` Y ) ) -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. b e. ( ( N Sat F ) ` Y ) x = ( ( 1st ` a ) |g ( 1st ` b ) ) ) )
37 36 rexlimdva 
 |-  ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) -> ( E. v e. ( ( M Sat E ) ` Y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) -> E. b e. ( ( N Sat F ) ` Y ) x = ( ( 1st ` a ) |g ( 1st ` b ) ) ) )
38 eqidd 
 |-  ( a = <. ( 1st ` u ) , s >. -> i = i )
39 38 23 goaleq12d 
 |-  ( a = <. ( 1st ` u ) , s >. -> A.g i ( 1st ` u ) = A.g i ( 1st ` a ) )
40 39 eqeq2d 
 |-  ( a = <. ( 1st ` u ) , s >. -> ( x = A.g i ( 1st ` u ) <-> x = A.g i ( 1st ` a ) ) )
41 40 biimpd 
 |-  ( a = <. ( 1st ` u ) , s >. -> ( x = A.g i ( 1st ` u ) -> x = A.g i ( 1st ` a ) ) )
42 41 adantl 
 |-  ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) -> ( x = A.g i ( 1st ` u ) -> x = A.g i ( 1st ` a ) ) )
43 42 reximdv 
 |-  ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) -> ( E. i e. _om x = A.g i ( 1st ` u ) -> E. i e. _om x = A.g i ( 1st ` a ) ) )
44 37 43 orim12d 
 |-  ( ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` Y ) ) /\ a = <. ( 1st ` u ) , s >. ) -> ( ( E. v e. ( ( M Sat E ) ` Y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) -> ( E. b e. ( ( N Sat F ) ` Y ) x = ( ( 1st ` a ) |g ( 1st ` b ) ) \/ E. i e. _om x = A.g i ( 1st ` a ) ) ) )
45 11 44 rspcimedv 
 |-  ( ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) /\ <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` 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 ) ) ) )
46 45 ex 
 |-  ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) -> ( <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` 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 ) ) ) ) )
47 46 exlimdv 
 |-  ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) -> ( E. s <. ( 1st ` u ) , s >. e. ( ( N Sat F ) ` 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 ) ) ) ) )
48 10 47 syl5bi 
 |-  ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) -> ( ( 1st ` u ) e. dom ( ( N Sat F ) ` 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 ) ) ) ) )
49 7 48 sylbid 
 |-  ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ u e. ( ( M Sat E ) ` Y ) ) -> ( ( 1st ` u ) e. dom ( ( 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 ) ) ) ) )
50 4 49 mpd 
 |-  ( ( ( ( M e. V /\ E e. W /\ Y e. _om ) /\ dom ( ( M Sat E ) ` Y ) = dom ( ( N Sat F ) ` Y ) ) /\ 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 ) ) ) )
51 50 rexlimdva 
 |-  ( ( ( 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 ) ) ) )