Metamath Proof Explorer

Theorem fmlafvel

Description: A class is a valid Godel formula of height N iff it is the first component of a member of the value of the satisfaction predicate as function over wff codes in the empty model with an empty binary relation at N . (Contributed by AV, 19-Sep-2023)

Ref Expression
Assertion fmlafvel 
|- ( N e. _om -> ( F e. ( Fmla ` N ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = (/) -> ( Fmla ` x ) = ( Fmla ` (/) ) )
2 1 eleq2d 
 |-  ( x = (/) -> ( F e. ( Fmla ` x ) <-> F e. ( Fmla ` (/) ) ) )
3 fveq2 
 |-  ( x = (/) -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` (/) ) )
4 3 eleq2d 
 |-  ( x = (/) -> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` (/) ) ) )
5 2 4 bibi12d 
 |-  ( x = (/) -> ( ( F e. ( Fmla ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) ) <-> ( F e. ( Fmla ` (/) ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` (/) ) ) ) )
6 5 imbi2d 
 |-  ( x = (/) -> ( ( F e. _V -> ( F e. ( Fmla ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) ) ) <-> ( F e. _V -> ( F e. ( Fmla ` (/) ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` (/) ) ) ) ) )
7 fveq2 
 |-  ( x = y -> ( Fmla ` x ) = ( Fmla ` y ) )
8 7 eleq2d 
 |-  ( x = y -> ( F e. ( Fmla ` x ) <-> F e. ( Fmla ` y ) ) )
9 fveq2 
 |-  ( x = y -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` y ) )
10 9 eleq2d 
 |-  ( x = y -> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) )
11 8 10 bibi12d 
 |-  ( x = y -> ( ( F e. ( Fmla ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) ) <-> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) )
12 11 imbi2d 
 |-  ( x = y -> ( ( F e. _V -> ( F e. ( Fmla ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) ) ) <-> ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) )
13 fveq2 
 |-  ( x = suc y -> ( Fmla ` x ) = ( Fmla ` suc y ) )
14 13 eleq2d 
 |-  ( x = suc y -> ( F e. ( Fmla ` x ) <-> F e. ( Fmla ` suc y ) ) )
15 fveq2 
 |-  ( x = suc y -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` suc y ) )
16 15 eleq2d 
 |-  ( x = suc y -> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` suc y ) ) )
17 14 16 bibi12d 
 |-  ( x = suc y -> ( ( F e. ( Fmla ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) ) <-> ( F e. ( Fmla ` suc y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` suc y ) ) ) )
18 17 imbi2d 
 |-  ( x = suc y -> ( ( F e. _V -> ( F e. ( Fmla ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) ) ) <-> ( F e. _V -> ( F e. ( Fmla ` suc y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` suc y ) ) ) ) )
19 fveq2 
 |-  ( x = N -> ( Fmla ` x ) = ( Fmla ` N ) )
20 19 eleq2d 
 |-  ( x = N -> ( F e. ( Fmla ` x ) <-> F e. ( Fmla ` N ) ) )
21 fveq2 
 |-  ( x = N -> ( ( (/) Sat (/) ) ` x ) = ( ( (/) Sat (/) ) ` N ) )
22 21 eleq2d 
 |-  ( x = N -> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )
23 20 22 bibi12d 
 |-  ( x = N -> ( ( F e. ( Fmla ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) ) <-> ( F e. ( Fmla ` N ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) )
24 23 imbi2d 
 |-  ( x = N -> ( ( F e. _V -> ( F e. ( Fmla ` x ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` x ) ) ) <-> ( F e. _V -> ( F e. ( Fmla ` N ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) ) )
25 eqeq1 
 |-  ( x = F -> ( x = ( i e.g j ) <-> F = ( i e.g j ) ) )
26 25 2rexbidv 
 |-  ( x = F -> ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> E. i e. _om E. j e. _om F = ( i e.g j ) ) )
27 26 elrab 
 |-  ( F e. { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } <-> ( F e. _V /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) )
28 eqidd 
 |-  ( ( F e. _V /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) -> (/) = (/) )
29 simpr 
 |-  ( ( F e. _V /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) -> E. i e. _om E. j e. _om F = ( i e.g j ) )
30 28 29 jca 
 |-  ( ( F e. _V /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) -> ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) )
31 simpr 
 |-  ( ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) -> E. i e. _om E. j e. _om F = ( i e.g j ) )
32 31 anim2i 
 |-  ( ( F e. _V /\ ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) ) -> ( F e. _V /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) )
33 32 ex 
 |-  ( F e. _V -> ( ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) -> ( F e. _V /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) ) )
34 30 33 impbid2 
 |-  ( F e. _V -> ( ( F e. _V /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) <-> ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) ) )
35 27 34 syl5bb 
 |-  ( F e. _V -> ( F e. { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } <-> ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) ) )
36 fmla0 
 |-  ( Fmla ` (/) ) = { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) }
37 36 eleq2i 
 |-  ( F e. ( Fmla ` (/) ) <-> F e. { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } )
38 37 a1i 
 |-  ( F e. _V -> ( F e. ( Fmla ` (/) ) <-> F e. { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } ) )
39 satf00 
 |-  ( ( (/) Sat (/) ) ` (/) ) = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) }
40 39 a1i 
 |-  ( F e. _V -> ( ( (/) Sat (/) ) ` (/) ) = { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } )
41 40 eleq2d 
 |-  ( F e. _V -> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` (/) ) <-> <. F , (/) >. e. { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) )
42 0ex 
 |-  (/) e. _V
43 eqeq1 
 |-  ( y = (/) -> ( y = (/) <-> (/) = (/) ) )
44 43 26 bi2anan9r 
 |-  ( ( x = F /\ y = (/) ) -> ( ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) <-> ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) ) )
45 44 opelopabga 
 |-  ( ( F e. _V /\ (/) e. _V ) -> ( <. F , (/) >. e. { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } <-> ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) ) )
46 42 45 mpan2 
 |-  ( F e. _V -> ( <. F , (/) >. e. { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } <-> ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) ) )
47 41 46 bitrd 
 |-  ( F e. _V -> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` (/) ) <-> ( (/) = (/) /\ E. i e. _om E. j e. _om F = ( i e.g j ) ) ) )
48 35 38 47 3bitr4d 
 |-  ( F e. _V -> ( F e. ( Fmla ` (/) ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` (/) ) ) )
49 eqid 
 |-  (/) = (/)
50 49 biantrur 
 |-  ( E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) <-> ( (/) = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) )
51 50 bicomi 
 |-  ( ( (/) = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) <-> E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) )
52 51 a1i 
 |-  ( F e. _V -> ( ( (/) = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) <-> E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) )
53 eqeq1 
 |-  ( z = (/) -> ( z = (/) <-> (/) = (/) ) )
54 eqeq1 
 |-  ( x = F -> ( x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> F = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
55 54 rexbidv 
 |-  ( x = F -> ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
56 eqeq1 
 |-  ( x = F -> ( x = A.g i ( 1st ` u ) <-> F = A.g i ( 1st ` u ) ) )
57 56 rexbidv 
 |-  ( x = F -> ( E. i e. _om x = A.g i ( 1st ` u ) <-> E. i e. _om F = A.g i ( 1st ` u ) ) )
58 55 57 orbi12d 
 |-  ( x = F -> ( ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) )
59 58 rexbidv 
 |-  ( x = F -> ( E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) )
60 53 59 bi2anan9r 
 |-  ( ( x = F /\ z = (/) ) -> ( ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) <-> ( (/) = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) ) )
61 60 opelopabga 
 |-  ( ( F e. _V /\ (/) e. _V ) -> ( <. F , (/) >. e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } <-> ( (/) = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) ) )
62 42 61 mpan2 
 |-  ( F e. _V -> ( <. F , (/) >. e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } <-> ( (/) = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) ) )
63 59 elabg 
 |-  ( F e. _V -> ( F e. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } <-> E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) F = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om F = A.g i ( 1st ` u ) ) ) )
64 52 62 63 3bitr4d 
 |-  ( F e. _V -> ( <. F , (/) >. e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } <-> F e. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) )
65 64 adantl 
 |-  ( ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) /\ F e. _V ) -> ( <. F , (/) >. e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } <-> F e. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) )
66 65 orbi2d 
 |-  ( ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) /\ F e. _V ) -> ( ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) \/ <. F , (/) >. e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) <-> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) \/ F e. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) ) )
67 eqid 
 |-  ( (/) Sat (/) ) = ( (/) Sat (/) )
68 67 satf0suc 
 |-  ( y e. _om -> ( ( (/) Sat (/) ) ` suc y ) = ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
69 68 eleq2d 
 |-  ( y e. _om -> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` suc y ) <-> <. F , (/) >. e. ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
70 elun 
 |-  ( <. F , (/) >. e. ( ( ( (/) Sat (/) ) ` y ) u. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) <-> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) \/ <. F , (/) >. e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
71 69 70 bitrdi 
 |-  ( y e. _om -> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` suc y ) <-> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) \/ <. F , (/) >. e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
72 71 ad2antrr 
 |-  ( ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) /\ F e. _V ) -> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` suc y ) <-> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) \/ <. F , (/) >. e. { <. x , z >. | ( z = (/) /\ E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
73 fmlasuc0 
 |-  ( y e. _om -> ( Fmla ` suc y ) = ( ( Fmla ` y ) u. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) )
74 73 eleq2d 
 |-  ( y e. _om -> ( F e. ( Fmla ` suc y ) <-> F e. ( ( Fmla ` y ) u. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) ) )
75 74 ad2antrr 
 |-  ( ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) /\ F e. _V ) -> ( F e. ( Fmla ` suc y ) <-> F e. ( ( Fmla ` y ) u. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) ) )
76 elun 
 |-  ( F e. ( ( Fmla ` y ) u. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) <-> ( F e. ( Fmla ` y ) \/ F e. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) )
77 76 a1i 
 |-  ( ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) /\ F e. _V ) -> ( F e. ( ( Fmla ` y ) u. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) <-> ( F e. ( Fmla ` y ) \/ F e. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) ) )
78 simpr 
 |-  ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) -> ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) )
79 78 imp 
 |-  ( ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) /\ F e. _V ) -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) )
80 79 orbi1d 
 |-  ( ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) /\ F e. _V ) -> ( ( F e. ( Fmla ` y ) \/ F e. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) <-> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) \/ F e. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) ) )
81 75 77 80 3bitrd 
 |-  ( ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) /\ F e. _V ) -> ( F e. ( Fmla ` suc y ) <-> ( <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) \/ F e. { x | E. u e. ( ( (/) Sat (/) ) ` y ) ( E. v e. ( ( (/) Sat (/) ) ` y ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) ) )
82 66 72 81 3bitr4rd 
 |-  ( ( ( y e. _om /\ ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) ) /\ F e. _V ) -> ( F e. ( Fmla ` suc y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` suc y ) ) )
83 82 exp31 
 |-  ( y e. _om -> ( ( F e. _V -> ( F e. ( Fmla ` y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` y ) ) ) -> ( F e. _V -> ( F e. ( Fmla ` suc y ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` suc y ) ) ) ) )
84 6 12 18 24 48 83 finds 
 |-  ( N e. _om -> ( F e. _V -> ( F e. ( Fmla ` N ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) )
85 84 com12 
 |-  ( F e. _V -> ( N e. _om -> ( F e. ( Fmla ` N ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) )
86 prcnel 
 |-  ( -. F e. _V -> -. F e. ( Fmla ` N ) )
87 86 adantr 
 |-  ( ( -. F e. _V /\ N e. _om ) -> -. F e. ( Fmla ` N ) )
88 opprc1 
 |-  ( -. F e. _V -> <. F , (/) >. = (/) )
89 88 adantr 
 |-  ( ( -. F e. _V /\ N e. _om ) -> <. F , (/) >. = (/) )
90 satf0n0 
 |-  ( N e. _om -> (/) e/ ( ( (/) Sat (/) ) ` N ) )
91 df-nel 
 |-  ( (/) e/ ( ( (/) Sat (/) ) ` N ) <-> -. (/) e. ( ( (/) Sat (/) ) ` N ) )
92 90 91 sylib 
 |-  ( N e. _om -> -. (/) e. ( ( (/) Sat (/) ) ` N ) )
93 92 adantl 
 |-  ( ( -. F e. _V /\ N e. _om ) -> -. (/) e. ( ( (/) Sat (/) ) ` N ) )
94 89 93 eqneltrd 
 |-  ( ( -. F e. _V /\ N e. _om ) -> -. <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) )
95 87 94 2falsed 
 |-  ( ( -. F e. _V /\ N e. _om ) -> ( F e. ( Fmla ` N ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )
96 95 ex 
 |-  ( -. F e. _V -> ( N e. _om -> ( F e. ( Fmla ` N ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) )
97 85 96 pm2.61i 
 |-  ( N e. _om -> ( F e. ( Fmla ` N ) <-> <. F , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )