Metamath Proof Explorer

Theorem fmlasuc0

Description: The valid Godel formulas of height ( N + 1 ) . (Contributed by AV, 18-Sep-2023)

Ref Expression
Assertion fmlasuc0 
|- ( N e. _om -> ( Fmla ` suc N ) = ( ( Fmla ` N ) u. { x | E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) )

Proof

Step Hyp Ref Expression
1 df-fmla 
 |-  Fmla = ( n e. suc _om |-> dom ( ( (/) Sat (/) ) ` n ) )
2 fveq2 
 |-  ( n = suc N -> ( ( (/) Sat (/) ) ` n ) = ( ( (/) Sat (/) ) ` suc N ) )
3 2 dmeqd 
 |-  ( n = suc N -> dom ( ( (/) Sat (/) ) ` n ) = dom ( ( (/) Sat (/) ) ` suc N ) )
4 omsucelsucb 
 |-  ( N e. _om <-> suc N e. suc _om )
5 4 biimpi 
 |-  ( N e. _om -> suc N e. suc _om )
6 fvex 
 |-  ( ( (/) Sat (/) ) ` suc N ) e. _V
7 6 dmex 
 |-  dom ( ( (/) Sat (/) ) ` suc N ) e. _V
8 7 a1i 
 |-  ( N e. _om -> dom ( ( (/) Sat (/) ) ` suc N ) e. _V )
9 1 3 5 8 fvmptd3 
 |-  ( N e. _om -> ( Fmla ` suc N ) = dom ( ( (/) Sat (/) ) ` suc N ) )
10 satf0sucom 
 |-  ( suc N e. suc _om -> ( ( (/) Sat (/) ) ` suc N ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc N ) )
11 5 10 syl 
 |-  ( N e. _om -> ( ( (/) Sat (/) ) ` suc N ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc N ) )
12 nnon 
 |-  ( N e. _om -> N e. On )
13 rdgsuc 
 |-  ( N e. On -> ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc N ) = ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) )
14 12 13 syl 
 |-  ( N e. _om -> ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` suc N ) = ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) )
15 11 14 eqtrd 
 |-  ( N e. _om -> ( ( (/) Sat (/) ) ` suc N ) = ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) )
16 15 dmeqd 
 |-  ( N e. _om -> dom ( ( (/) Sat (/) ) ` suc N ) = dom ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) )
17 elelsuc 
 |-  ( N e. _om -> N e. suc _om )
18 satf0sucom 
 |-  ( N e. suc _om -> ( ( (/) Sat (/) ) ` N ) = ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) )
19 18 eqcomd 
 |-  ( N e. suc _om -> ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) = ( ( (/) Sat (/) ) ` N ) )
20 17 19 syl 
 |-  ( N e. _om -> ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) = ( ( (/) Sat (/) ) ` N ) )
21 20 fveq2d 
 |-  ( N e. _om -> ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) = ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( ( (/) Sat (/) ) ` N ) ) )
22 eqidd 
 |-  ( N e. _om -> ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) = ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) )
23 id 
 |-  ( f = ( ( (/) Sat (/) ) ` N ) -> f = ( ( (/) Sat (/) ) ` N ) )
24 rexeq 
 |-  ( f = ( ( (/) Sat (/) ) ` N ) -> ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) <-> E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) ) )
25 24 orbi1d 
 |-  ( f = ( ( (/) Sat (/) ) ` N ) -> ( ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
26 25 rexeqbi1dv 
 |-  ( f = ( ( (/) Sat (/) ) ` N ) -> ( E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) <-> E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
27 26 anbi2d 
 |-  ( f = ( ( (/) Sat (/) ) ` N ) -> ( ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) <-> ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) )
28 27 opabbidv 
 |-  ( f = ( ( (/) Sat (/) ) ` N ) -> { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } = { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } )
29 23 28 uneq12d 
 |-  ( f = ( ( (/) Sat (/) ) ` N ) -> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) = ( ( ( (/) Sat (/) ) ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
30 29 adantl 
 |-  ( ( N e. _om /\ f = ( ( (/) Sat (/) ) ` N ) ) -> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) = ( ( ( (/) Sat (/) ) ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
31 fvex 
 |-  ( ( (/) Sat (/) ) ` N ) e. _V
32 31 a1i 
 |-  ( N e. _om -> ( ( (/) Sat (/) ) ` N ) e. _V )
33 peano1 
 |-  (/) e. _om
34 eleq1 
 |-  ( y = (/) -> ( y e. _om <-> (/) e. _om ) )
35 33 34 mpbiri 
 |-  ( y = (/) -> y e. _om )
36 35 adantr 
 |-  ( ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) -> y e. _om )
37 36 pm4.71ri 
 |-  ( ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) <-> ( y e. _om /\ ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) )
38 37 opabbii 
 |-  { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } = { <. x , y >. | ( y e. _om /\ ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) }
39 omex 
 |-  _om e. _V
40 id 
 |-  ( _om e. _V -> _om e. _V )
41 unab 
 |-  ( { x | E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) } u. { x | E. i e. _om x = A.g i ( 1st ` u ) } ) = { x | ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) }
42 31 abrexex 
 |-  { x | E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) } e. _V
43 39 abrexex 
 |-  { x | E. i e. _om x = A.g i ( 1st ` u ) } e. _V
44 42 43 unex 
 |-  ( { x | E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) } u. { x | E. i e. _om x = A.g i ( 1st ` u ) } ) e. _V
45 41 44 eqeltrri 
 |-  { x | ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } e. _V
46 45 a1i 
 |-  ( ( ( _om e. _V /\ y e. _om ) /\ u e. ( ( (/) Sat (/) ) ` N ) ) -> { x | ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } e. _V )
47 46 ralrimiva 
 |-  ( ( _om e. _V /\ y e. _om ) -> A. u e. ( ( (/) Sat (/) ) ` N ) { x | ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } e. _V )
48 abrexex2g 
 |-  ( ( ( ( (/) Sat (/) ) ` N ) e. _V /\ A. u e. ( ( (/) Sat (/) ) ` N ) { x | ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } e. _V ) -> { x | E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } e. _V )
49 31 47 48 sylancr 
 |-  ( ( _om e. _V /\ y e. _om ) -> { x | E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } e. _V )
50 40 49 opabex3rd 
 |-  ( _om e. _V -> { <. x , y >. | ( y e. _om /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } e. _V )
51 39 50 ax-mp 
 |-  { <. x , y >. | ( y e. _om /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } e. _V
52 simpr 
 |-  ( ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) -> E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) )
53 52 anim2i 
 |-  ( ( y e. _om /\ ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) -> ( y e. _om /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
54 53 ssopab2i 
 |-  { <. x , y >. | ( y e. _om /\ ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) } C_ { <. x , y >. | ( y e. _om /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) }
55 51 54 ssexi 
 |-  { <. x , y >. | ( y e. _om /\ ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) } e. _V
56 55 a1i 
 |-  ( N e. _om -> { <. x , y >. | ( y e. _om /\ ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) ) } e. _V )
57 38 56 eqeltrid 
 |-  ( N e. _om -> { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } e. _V )
58 unexg 
 |-  ( ( ( ( (/) Sat (/) ) ` N ) e. _V /\ { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } e. _V ) -> ( ( ( (/) Sat (/) ) ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) e. _V )
59 31 57 58 sylancr 
 |-  ( N e. _om -> ( ( ( (/) Sat (/) ) ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) e. _V )
60 22 30 32 59 fvmptd 
 |-  ( N e. _om -> ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( ( (/) Sat (/) ) ` N ) ) = ( ( ( (/) Sat (/) ) ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
61 21 60 eqtrd 
 |-  ( N e. _om -> ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) = ( ( ( (/) Sat (/) ) ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
62 61 dmeqd 
 |-  ( N e. _om -> dom ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) = dom ( ( ( (/) Sat (/) ) ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
63 dmun 
 |-  dom ( ( ( (/) Sat (/) ) ` N ) u. { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) = ( dom ( ( (/) Sat (/) ) ` N ) u. dom { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } )
64 62 63 eqtrdi 
 |-  ( N e. _om -> dom ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) = ( dom ( ( (/) Sat (/) ) ` N ) u. dom { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) )
65 fmlafv 
 |-  ( N e. suc _om -> ( Fmla ` N ) = dom ( ( (/) Sat (/) ) ` N ) )
66 17 65 syl 
 |-  ( N e. _om -> ( Fmla ` N ) = dom ( ( (/) Sat (/) ) ` N ) )
67 66 eqcomd 
 |-  ( N e. _om -> dom ( ( (/) Sat (/) ) ` N ) = ( Fmla ` N ) )
68 dmopab 
 |-  dom { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } = { x | E. y ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) }
69 68 a1i 
 |-  ( N e. _om -> dom { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } = { x | E. y ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } )
70 0ex 
 |-  (/) e. _V
71 70 isseti 
 |-  E. y y = (/)
72 19.41v 
 |-  ( E. y ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) <-> ( E. y y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) )
73 71 72 mpbiran 
 |-  ( E. y ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) <-> E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) )
74 73 abbii 
 |-  { x | E. y ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } = { x | E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) }
75 69 74 eqtrdi 
 |-  ( N e. _om -> dom { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } = { x | E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } )
76 67 75 uneq12d 
 |-  ( N e. _om -> ( dom ( ( (/) Sat (/) ) ` N ) u. dom { <. x , y >. | ( y = (/) /\ E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) = ( ( Fmla ` N ) u. { x | E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) )
77 64 76 eqtrd 
 |-  ( N e. _om -> dom ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) ` ( rec ( ( f e. _V |-> ( f u. { <. x , y >. | ( y = (/) /\ E. u e. f ( E. v e. f x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) ) } ) ) , { <. x , y >. | ( y = (/) /\ E. i e. _om E. j e. _om x = ( i e.g j ) ) } ) ` N ) ) = ( ( Fmla ` N ) u. { x | E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) )
78 9 16 77 3eqtrd 
 |-  ( N e. _om -> ( Fmla ` suc N ) = ( ( Fmla ` N ) u. { x | E. u e. ( ( (/) Sat (/) ) ` N ) ( E. v e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` u ) |g ( 1st ` v ) ) \/ E. i e. _om x = A.g i ( 1st ` u ) ) } ) )