Metamath Proof Explorer

Theorem satfrnmapom

Description: The range of the satisfaction predicate as function over wff codes in any model M and any binary relation E on M for a natural number N is a subset of the power set of all mappings from the natural numbers into the model M . (Contributed by AV, 13-Oct-2023)

Ref Expression
Assertion satfrnmapom 
|- ( ( M e. V /\ E e. W /\ N e. _om ) -> ran ( ( M Sat E ) ` N ) C_ ~P ( M ^m _om ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( a = (/) -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` (/) ) )
2 1 rneqd 
 |-  ( a = (/) -> ran ( ( M Sat E ) ` a ) = ran ( ( M Sat E ) ` (/) ) )
3 2 eleq2d 
 |-  ( a = (/) -> ( n e. ran ( ( M Sat E ) ` a ) <-> n e. ran ( ( M Sat E ) ` (/) ) ) )
4 3 imbi1d 
 |-  ( a = (/) -> ( ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) <-> ( n e. ran ( ( M Sat E ) ` (/) ) -> n e. ~P ( M ^m _om ) ) ) )
5 4 imbi2d 
 |-  ( a = (/) -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) ) <-> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` (/) ) -> n e. ~P ( M ^m _om ) ) ) ) )
6 fveq2 
 |-  ( a = b -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` b ) )
7 6 rneqd 
 |-  ( a = b -> ran ( ( M Sat E ) ` a ) = ran ( ( M Sat E ) ` b ) )
8 7 eleq2d 
 |-  ( a = b -> ( n e. ran ( ( M Sat E ) ` a ) <-> n e. ran ( ( M Sat E ) ` b ) ) )
9 8 imbi1d 
 |-  ( a = b -> ( ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) <-> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) )
10 9 imbi2d 
 |-  ( a = b -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) ) <-> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) )
11 fveq2 
 |-  ( a = suc b -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` suc b ) )
12 11 rneqd 
 |-  ( a = suc b -> ran ( ( M Sat E ) ` a ) = ran ( ( M Sat E ) ` suc b ) )
13 12 eleq2d 
 |-  ( a = suc b -> ( n e. ran ( ( M Sat E ) ` a ) <-> n e. ran ( ( M Sat E ) ` suc b ) ) )
14 13 imbi1d 
 |-  ( a = suc b -> ( ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) <-> ( n e. ran ( ( M Sat E ) ` suc b ) -> n e. ~P ( M ^m _om ) ) ) )
15 14 imbi2d 
 |-  ( a = suc b -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) ) <-> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` suc b ) -> n e. ~P ( M ^m _om ) ) ) ) )
16 fveq2 
 |-  ( a = N -> ( ( M Sat E ) ` a ) = ( ( M Sat E ) ` N ) )
17 16 rneqd 
 |-  ( a = N -> ran ( ( M Sat E ) ` a ) = ran ( ( M Sat E ) ` N ) )
18 17 eleq2d 
 |-  ( a = N -> ( n e. ran ( ( M Sat E ) ` a ) <-> n e. ran ( ( M Sat E ) ` N ) ) )
19 18 imbi1d 
 |-  ( a = N -> ( ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) <-> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) ) )
20 19 imbi2d 
 |-  ( a = N -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` a ) -> n e. ~P ( M ^m _om ) ) ) <-> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) ) ) )
21 eqid 
 |-  ( M Sat E ) = ( M Sat E )
22 21 satfv0 
 |-  ( ( M e. V /\ E e. W ) -> ( ( M Sat E ) ` (/) ) = { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } )
23 22 rneqd 
 |-  ( ( M e. V /\ E e. W ) -> ran ( ( M Sat E ) ` (/) ) = ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } )
24 23 eleq2d 
 |-  ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` (/) ) <-> n e. ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } ) )
25 rnopab 
 |-  ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } = { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) }
26 25 eleq2i 
 |-  ( n e. ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } <-> n e. { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } )
27 vex 
 |-  n e. _V
28 eqeq1 
 |-  ( y = n -> ( y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } <-> n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) )
29 28 anbi2d 
 |-  ( y = n -> ( ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) )
30 29 2rexbidv 
 |-  ( y = n -> ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) )
31 30 exbidv 
 |-  ( y = n -> ( E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) <-> E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) ) )
32 27 31 elab 
 |-  ( n e. { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } <-> E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) )
33 ovex 
 |-  ( M ^m _om ) e. _V
34 ssrab2 
 |-  { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } C_ ( M ^m _om )
35 33 34 elpwi2 
 |-  { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } e. ~P ( M ^m _om )
36 eleq1 
 |-  ( n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> ( n e. ~P ( M ^m _om ) <-> { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } e. ~P ( M ^m _om ) ) )
37 35 36 mpbiri 
 |-  ( n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } -> n e. ~P ( M ^m _om ) )
38 37 adantl 
 |-  ( ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> n e. ~P ( M ^m _om ) )
39 38 a1i 
 |-  ( ( i e. _om /\ j e. _om ) -> ( ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> n e. ~P ( M ^m _om ) ) )
40 39 rexlimivv 
 |-  ( E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> n e. ~P ( M ^m _om ) )
41 40 exlimiv 
 |-  ( E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ n = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) -> n e. ~P ( M ^m _om ) )
42 32 41 sylbi 
 |-  ( n e. { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } -> n e. ~P ( M ^m _om ) )
43 42 a1i 
 |-  ( ( M e. V /\ E e. W ) -> ( n e. { y | E. x E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } -> n e. ~P ( M ^m _om ) ) )
44 26 43 syl5bi 
 |-  ( ( M e. V /\ E e. W ) -> ( n e. ran { <. x , y >. | E. i e. _om E. j e. _om ( x = ( i e.g j ) /\ y = { f e. ( M ^m _om ) | ( f ` i ) E ( f ` j ) } ) } -> n e. ~P ( M ^m _om ) ) )
45 24 44 sylbid 
 |-  ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` (/) ) -> n e. ~P ( M ^m _om ) ) )
46 21 satfvsuc 
 |-  ( ( M e. V /\ E e. W /\ b e. _om ) -> ( ( M Sat E ) ` suc b ) = ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
47 46 3expa 
 |-  ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ( ( M Sat E ) ` suc b ) = ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
48 47 rneqd 
 |-  ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ran ( ( M Sat E ) ` suc b ) = ran ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
49 rnun 
 |-  ran ( ( ( M Sat E ) ` b ) u. { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) = ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } )
50 48 49 eqtrdi 
 |-  ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ran ( ( M Sat E ) ` suc b ) = ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
51 50 eleq2d 
 |-  ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> n e. ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) ) )
52 elun 
 |-  ( n e. ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ n e. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) )
53 rnopab 
 |-  ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } = { y | E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) }
54 53 eleq2i 
 |-  ( n e. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } <-> n e. { y | E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } )
55 eqeq1 
 |-  ( y = n -> ( y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) <-> n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) )
56 55 anbi2d 
 |-  ( y = n -> ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) )
57 56 rexbidv 
 |-  ( y = n -> ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ y = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) <-> E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) )
58 eqeq1 
 |-  ( y = n -> ( y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } <-> n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) )
59 58 anbi2d 
 |-  ( y = n -> ( ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
60 59 rexbidv 
 |-  ( y = n -> ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ y = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) <-> E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
61 57 60 orbi12d 
 |-  ( y = n -> ( ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
62 61 rexbidv 
 |-  ( y = n -> ( E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
63 62 exbidv 
 |-  ( y = n -> ( E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) <-> E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
64 27 63 elab 
 |-  ( n e. { y | E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } <-> E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
65 54 64 bitri 
 |-  ( n e. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } <-> E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) )
66 65 orbi2i 
 |-  ( ( n e. ran ( ( M Sat E ) ` b ) \/ n e. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
67 52 66 bitri 
 |-  ( n e. ( ran ( ( M Sat E ) ` b ) u. ran { <. x , y >. | E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( 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 = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) } ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) )
68 51 67 bitrdi 
 |-  ( ( ( M e. V /\ E e. W ) /\ b e. _om ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
69 68 expcom 
 |-  ( b e. _om -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) ) )
70 69 adantr 
 |-  ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) ) )
71 70 imp 
 |-  ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( n e. ran ( ( M Sat E ) ` suc b ) <-> ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) ) )
72 simpr 
 |-  ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) )
73 72 imp 
 |-  ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) )
74 difss 
 |-  ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) C_ ( M ^m _om )
75 33 74 elpwi2 
 |-  ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. ~P ( M ^m _om )
76 eleq1 
 |-  ( n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> ( n e. ~P ( M ^m _om ) <-> ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) e. ~P ( M ^m _om ) ) )
77 75 76 mpbiri 
 |-  ( n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) -> n e. ~P ( M ^m _om ) )
78 77 adantl 
 |-  ( ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> n e. ~P ( M ^m _om ) )
79 78 adantl 
 |-  ( ( v e. ( ( M Sat E ) ` b ) /\ ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) ) -> n e. ~P ( M ^m _om ) )
80 79 rexlimiva 
 |-  ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) -> n e. ~P ( M ^m _om ) )
81 ssrab2 
 |-  { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } C_ ( M ^m _om )
82 33 81 elpwi2 
 |-  { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. ~P ( M ^m _om )
83 eleq1 
 |-  ( n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> ( n e. ~P ( M ^m _om ) <-> { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } e. ~P ( M ^m _om ) ) )
84 82 83 mpbiri 
 |-  ( n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } -> n e. ~P ( M ^m _om ) )
85 84 adantl 
 |-  ( ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> n e. ~P ( M ^m _om ) )
86 85 a1i 
 |-  ( i e. _om -> ( ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> n e. ~P ( M ^m _om ) ) )
87 86 rexlimiv 
 |-  ( E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) -> n e. ~P ( M ^m _om ) )
88 80 87 jaoi 
 |-  ( ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) )
89 88 a1i 
 |-  ( u e. ( ( M Sat E ) ` b ) -> ( ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) ) )
90 89 rexlimiv 
 |-  ( E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) )
91 90 exlimiv 
 |-  ( E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) )
92 91 a1i 
 |-  ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) -> n e. ~P ( M ^m _om ) ) )
93 73 92 jaod 
 |-  ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( ( n e. ran ( ( M Sat E ) ` b ) \/ E. x E. u e. ( ( M Sat E ) ` b ) ( E. v e. ( ( M Sat E ) ` b ) ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) /\ n = ( ( M ^m _om ) \ ( ( 2nd ` u ) i^i ( 2nd ` v ) ) ) ) \/ E. i e. _om ( x = A.g i ( 1st ` u ) /\ n = { a e. ( M ^m _om ) | A. z e. M ( { <. i , z >. } u. ( a |` ( _om \ { i } ) ) ) e. ( 2nd ` u ) } ) ) ) -> n e. ~P ( M ^m _om ) ) )
94 71 93 sylbid 
 |-  ( ( ( b e. _om /\ ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) ) /\ ( M e. V /\ E e. W ) ) -> ( n e. ran ( ( M Sat E ) ` suc b ) -> n e. ~P ( M ^m _om ) ) )
95 94 exp31 
 |-  ( b e. _om -> ( ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` b ) -> n e. ~P ( M ^m _om ) ) ) -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` suc b ) -> n e. ~P ( M ^m _om ) ) ) ) )
96 5 10 15 20 45 95 finds 
 |-  ( N e. _om -> ( ( M e. V /\ E e. W ) -> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) ) )
97 96 com12 
 |-  ( ( M e. V /\ E e. W ) -> ( N e. _om -> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) ) )
98 97 3impia 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ( n e. ran ( ( M Sat E ) ` N ) -> n e. ~P ( M ^m _om ) ) )
99 98 ssrdv 
 |-  ( ( M e. V /\ E e. W /\ N e. _om ) -> ran ( ( M Sat E ) ` N ) C_ ~P ( M ^m _om ) )