This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fmlasuc

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

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

Proof

Step Hyp Ref Expression
1 fmlasuc0 
 |-  ( N e. _om -> ( Fmla ` suc N ) = ( ( Fmla ` N ) u. { x | E. y e. ( ( (/) Sat (/) ) ` N ) ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) } ) )
2 eqid 
 |-  ( (/) Sat (/) ) = ( (/) Sat (/) )
3 2 satf0op 
 |-  ( N e. _om -> ( y e. ( ( (/) Sat (/) ) ` N ) <-> E. z ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) )
4 fveq2 
 |-  ( z = w -> ( 1st ` z ) = ( 1st ` w ) )
5 4 oveq2d 
 |-  ( z = w -> ( ( 1st ` y ) |g ( 1st ` z ) ) = ( ( 1st ` y ) |g ( 1st ` w ) ) )
6 5 eqeq2d 
 |-  ( z = w -> ( x = ( ( 1st ` y ) |g ( 1st ` z ) ) <-> x = ( ( 1st ` y ) |g ( 1st ` w ) ) ) )
7 6 cbvrexvw 
 |-  ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) <-> E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) )
8 7 orbi1i 
 |-  ( ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) <-> ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) )
9 fmlafvel 
 |-  ( N e. _om -> ( z e. ( Fmla ` N ) <-> <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )
10 9 biimprd 
 |-  ( N e. _om -> ( <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) -> z e. ( Fmla ` N ) ) )
11 10 adantld 
 |-  ( N e. _om -> ( ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) -> z e. ( Fmla ` N ) ) )
12 11 imp 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> z e. ( Fmla ` N ) )
13 vex 
 |-  z e. _V
14 0ex 
 |-  (/) e. _V
15 13 14 op1std 
 |-  ( y = <. z , (/) >. -> ( 1st ` y ) = z )
16 15 eleq1d 
 |-  ( y = <. z , (/) >. -> ( ( 1st ` y ) e. ( Fmla ` N ) <-> z e. ( Fmla ` N ) ) )
17 16 ad2antrl 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> ( ( 1st ` y ) e. ( Fmla ` N ) <-> z e. ( Fmla ` N ) ) )
18 12 17 mpbird 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> ( 1st ` y ) e. ( Fmla ` N ) )
19 18 3adant3 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) /\ ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) ) -> ( 1st ` y ) e. ( Fmla ` N ) )
20 oveq1 
 |-  ( u = ( 1st ` y ) -> ( u |g v ) = ( ( 1st ` y ) |g v ) )
21 20 eqeq2d 
 |-  ( u = ( 1st ` y ) -> ( x = ( u |g v ) <-> x = ( ( 1st ` y ) |g v ) ) )
22 21 rexbidv 
 |-  ( u = ( 1st ` y ) -> ( E. v e. ( Fmla ` N ) x = ( u |g v ) <-> E. v e. ( Fmla ` N ) x = ( ( 1st ` y ) |g v ) ) )
23 eqidd 
 |-  ( u = ( 1st ` y ) -> i = i )
24 id 
 |-  ( u = ( 1st ` y ) -> u = ( 1st ` y ) )
25 23 24 goaleq12d 
 |-  ( u = ( 1st ` y ) -> A.g i u = A.g i ( 1st ` y ) )
26 25 eqeq2d 
 |-  ( u = ( 1st ` y ) -> ( x = A.g i u <-> x = A.g i ( 1st ` y ) ) )
27 26 rexbidv 
 |-  ( u = ( 1st ` y ) -> ( E. i e. _om x = A.g i u <-> E. i e. _om x = A.g i ( 1st ` y ) ) )
28 22 27 orbi12d 
 |-  ( u = ( 1st ` y ) -> ( ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) <-> ( E. v e. ( Fmla ` N ) x = ( ( 1st ` y ) |g v ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) ) )
29 28 adantl 
 |-  ( ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) /\ ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) ) /\ u = ( 1st ` y ) ) -> ( ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) <-> ( E. v e. ( Fmla ` N ) x = ( ( 1st ` y ) |g v ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) ) )
30 2 satf0op 
 |-  ( N e. _om -> ( w e. ( ( (/) Sat (/) ) ` N ) <-> E. y ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) )
31 fmlafvel 
 |-  ( N e. _om -> ( y e. ( Fmla ` N ) <-> <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )
32 31 biimprd 
 |-  ( N e. _om -> ( <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) -> y e. ( Fmla ` N ) ) )
33 32 adantld 
 |-  ( N e. _om -> ( ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) -> y e. ( Fmla ` N ) ) )
34 33 imp 
 |-  ( ( N e. _om /\ ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> y e. ( Fmla ` N ) )
35 vex 
 |-  y e. _V
36 35 14 op1std 
 |-  ( w = <. y , (/) >. -> ( 1st ` w ) = y )
37 36 eleq1d 
 |-  ( w = <. y , (/) >. -> ( ( 1st ` w ) e. ( Fmla ` N ) <-> y e. ( Fmla ` N ) ) )
38 37 ad2antrl 
 |-  ( ( N e. _om /\ ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> ( ( 1st ` w ) e. ( Fmla ` N ) <-> y e. ( Fmla ` N ) ) )
39 34 38 mpbird 
 |-  ( ( N e. _om /\ ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> ( 1st ` w ) e. ( Fmla ` N ) )
40 39 adantr 
 |-  ( ( ( N e. _om /\ ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) /\ x = ( z |g ( 1st ` w ) ) ) -> ( 1st ` w ) e. ( Fmla ` N ) )
41 oveq2 
 |-  ( v = ( 1st ` w ) -> ( z |g v ) = ( z |g ( 1st ` w ) ) )
42 41 eqeq2d 
 |-  ( v = ( 1st ` w ) -> ( x = ( z |g v ) <-> x = ( z |g ( 1st ` w ) ) ) )
43 42 adantl 
 |-  ( ( ( ( N e. _om /\ ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) /\ x = ( z |g ( 1st ` w ) ) ) /\ v = ( 1st ` w ) ) -> ( x = ( z |g v ) <-> x = ( z |g ( 1st ` w ) ) ) )
44 simpr 
 |-  ( ( ( N e. _om /\ ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) /\ x = ( z |g ( 1st ` w ) ) ) -> x = ( z |g ( 1st ` w ) ) )
45 40 43 44 rspcedvd 
 |-  ( ( ( N e. _om /\ ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) /\ x = ( z |g ( 1st ` w ) ) ) -> E. v e. ( Fmla ` N ) x = ( z |g v ) )
46 45 exp31 
 |-  ( N e. _om -> ( ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) -> ( x = ( z |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( z |g v ) ) ) )
47 46 exlimdv 
 |-  ( N e. _om -> ( E. y ( w = <. y , (/) >. /\ <. y , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) -> ( x = ( z |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( z |g v ) ) ) )
48 30 47 sylbid 
 |-  ( N e. _om -> ( w e. ( ( (/) Sat (/) ) ` N ) -> ( x = ( z |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( z |g v ) ) ) )
49 48 rexlimdv 
 |-  ( N e. _om -> ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( z |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( z |g v ) ) )
50 49 adantr 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( z |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( z |g v ) ) )
51 15 oveq1d 
 |-  ( y = <. z , (/) >. -> ( ( 1st ` y ) |g ( 1st ` w ) ) = ( z |g ( 1st ` w ) ) )
52 51 eqeq2d 
 |-  ( y = <. z , (/) >. -> ( x = ( ( 1st ` y ) |g ( 1st ` w ) ) <-> x = ( z |g ( 1st ` w ) ) ) )
53 52 rexbidv 
 |-  ( y = <. z , (/) >. -> ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) <-> E. w e. ( ( (/) Sat (/) ) ` N ) x = ( z |g ( 1st ` w ) ) ) )
54 15 oveq1d 
 |-  ( y = <. z , (/) >. -> ( ( 1st ` y ) |g v ) = ( z |g v ) )
55 54 eqeq2d 
 |-  ( y = <. z , (/) >. -> ( x = ( ( 1st ` y ) |g v ) <-> x = ( z |g v ) ) )
56 55 rexbidv 
 |-  ( y = <. z , (/) >. -> ( E. v e. ( Fmla ` N ) x = ( ( 1st ` y ) |g v ) <-> E. v e. ( Fmla ` N ) x = ( z |g v ) ) )
57 53 56 imbi12d 
 |-  ( y = <. z , (/) >. -> ( ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( ( 1st ` y ) |g v ) ) <-> ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( z |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( z |g v ) ) ) )
58 57 ad2antrl 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> ( ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( ( 1st ` y ) |g v ) ) <-> ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( z |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( z |g v ) ) ) )
59 50 58 mpbird 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) -> E. v e. ( Fmla ` N ) x = ( ( 1st ` y ) |g v ) ) )
60 59 orim1d 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) ) -> ( ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) -> ( E. v e. ( Fmla ` N ) x = ( ( 1st ` y ) |g v ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) ) )
61 60 3impia 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) /\ ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) ) -> ( E. v e. ( Fmla ` N ) x = ( ( 1st ` y ) |g v ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) )
62 19 29 61 rspcedvd 
 |-  ( ( N e. _om /\ ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) /\ ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) ) -> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) )
63 62 3exp 
 |-  ( N e. _om -> ( ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) -> ( ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) -> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) ) )
64 63 exlimdv 
 |-  ( N e. _om -> ( E. z ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) -> ( ( E. w e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` w ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) -> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) ) )
65 8 64 syl7bi 
 |-  ( N e. _om -> ( E. z ( y = <. z , (/) >. /\ <. z , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) -> ( ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) -> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) ) )
66 3 65 sylbid 
 |-  ( N e. _om -> ( y e. ( ( (/) Sat (/) ) ` N ) -> ( ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) -> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) ) )
67 66 rexlimdv 
 |-  ( N e. _om -> ( E. y e. ( ( (/) Sat (/) ) ` N ) ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) -> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) )
68 fmlafvel 
 |-  ( N e. _om -> ( u e. ( Fmla ` N ) <-> <. u , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )
69 68 biimpa 
 |-  ( ( N e. _om /\ u e. ( Fmla ` N ) ) -> <. u , (/) >. e. ( ( (/) Sat (/) ) ` N ) )
70 69 adantr 
 |-  ( ( ( N e. _om /\ u e. ( Fmla ` N ) ) /\ ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) -> <. u , (/) >. e. ( ( (/) Sat (/) ) ` N ) )
71 vex 
 |-  u e. _V
72 71 14 op1std 
 |-  ( y = <. u , (/) >. -> ( 1st ` y ) = u )
73 72 oveq1d 
 |-  ( y = <. u , (/) >. -> ( ( 1st ` y ) |g ( 1st ` z ) ) = ( u |g ( 1st ` z ) ) )
74 73 eqeq2d 
 |-  ( y = <. u , (/) >. -> ( x = ( ( 1st ` y ) |g ( 1st ` z ) ) <-> x = ( u |g ( 1st ` z ) ) ) )
75 74 rexbidv 
 |-  ( y = <. u , (/) >. -> ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) <-> E. z e. ( ( (/) Sat (/) ) ` N ) x = ( u |g ( 1st ` z ) ) ) )
76 eqidd 
 |-  ( y = <. u , (/) >. -> i = i )
77 76 72 goaleq12d 
 |-  ( y = <. u , (/) >. -> A.g i ( 1st ` y ) = A.g i u )
78 77 eqeq2d 
 |-  ( y = <. u , (/) >. -> ( x = A.g i ( 1st ` y ) <-> x = A.g i u ) )
79 78 rexbidv 
 |-  ( y = <. u , (/) >. -> ( E. i e. _om x = A.g i ( 1st ` y ) <-> E. i e. _om x = A.g i u ) )
80 75 79 orbi12d 
 |-  ( y = <. u , (/) >. -> ( ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) <-> ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( u |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i u ) ) )
81 80 adantl 
 |-  ( ( ( ( N e. _om /\ u e. ( Fmla ` N ) ) /\ ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) /\ y = <. u , (/) >. ) -> ( ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) <-> ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( u |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i u ) ) )
82 fmlafvel 
 |-  ( N e. _om -> ( v e. ( Fmla ` N ) <-> <. v , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )
83 82 biimpd 
 |-  ( N e. _om -> ( v e. ( Fmla ` N ) -> <. v , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )
84 83 adantr 
 |-  ( ( N e. _om /\ u e. ( Fmla ` N ) ) -> ( v e. ( Fmla ` N ) -> <. v , (/) >. e. ( ( (/) Sat (/) ) ` N ) ) )
85 84 imp 
 |-  ( ( ( N e. _om /\ u e. ( Fmla ` N ) ) /\ v e. ( Fmla ` N ) ) -> <. v , (/) >. e. ( ( (/) Sat (/) ) ` N ) )
86 85 adantr 
 |-  ( ( ( ( N e. _om /\ u e. ( Fmla ` N ) ) /\ v e. ( Fmla ` N ) ) /\ x = ( u |g v ) ) -> <. v , (/) >. e. ( ( (/) Sat (/) ) ` N ) )
87 vex 
 |-  v e. _V
88 87 14 op1std 
 |-  ( z = <. v , (/) >. -> ( 1st ` z ) = v )
89 88 oveq2d 
 |-  ( z = <. v , (/) >. -> ( u |g ( 1st ` z ) ) = ( u |g v ) )
90 89 eqeq2d 
 |-  ( z = <. v , (/) >. -> ( x = ( u |g ( 1st ` z ) ) <-> x = ( u |g v ) ) )
91 90 adantl 
 |-  ( ( ( ( ( N e. _om /\ u e. ( Fmla ` N ) ) /\ v e. ( Fmla ` N ) ) /\ x = ( u |g v ) ) /\ z = <. v , (/) >. ) -> ( x = ( u |g ( 1st ` z ) ) <-> x = ( u |g v ) ) )
92 simpr 
 |-  ( ( ( ( N e. _om /\ u e. ( Fmla ` N ) ) /\ v e. ( Fmla ` N ) ) /\ x = ( u |g v ) ) -> x = ( u |g v ) )
93 86 91 92 rspcedvd 
 |-  ( ( ( ( N e. _om /\ u e. ( Fmla ` N ) ) /\ v e. ( Fmla ` N ) ) /\ x = ( u |g v ) ) -> E. z e. ( ( (/) Sat (/) ) ` N ) x = ( u |g ( 1st ` z ) ) )
94 93 rexlimdva2 
 |-  ( ( N e. _om /\ u e. ( Fmla ` N ) ) -> ( E. v e. ( Fmla ` N ) x = ( u |g v ) -> E. z e. ( ( (/) Sat (/) ) ` N ) x = ( u |g ( 1st ` z ) ) ) )
95 94 orim1d 
 |-  ( ( N e. _om /\ u e. ( Fmla ` N ) ) -> ( ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) -> ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( u |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i u ) ) )
96 95 imp 
 |-  ( ( ( N e. _om /\ u e. ( Fmla ` N ) ) /\ ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) -> ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( u |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i u ) )
97 70 81 96 rspcedvd 
 |-  ( ( ( N e. _om /\ u e. ( Fmla ` N ) ) /\ ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) -> E. y e. ( ( (/) Sat (/) ) ` N ) ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) )
98 97 rexlimdva2 
 |-  ( N e. _om -> ( E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) -> E. y e. ( ( (/) Sat (/) ) ` N ) ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) ) )
99 67 98 impbid 
 |-  ( N e. _om -> ( E. y e. ( ( (/) Sat (/) ) ` N ) ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) <-> E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) )
100 99 abbidv 
 |-  ( N e. _om -> { x | E. y e. ( ( (/) Sat (/) ) ` N ) ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) } = { x | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } )
101 100 uneq2d 
 |-  ( N e. _om -> ( ( Fmla ` N ) u. { x | E. y e. ( ( (/) Sat (/) ) ` N ) ( E. z e. ( ( (/) Sat (/) ) ` N ) x = ( ( 1st ` y ) |g ( 1st ` z ) ) \/ E. i e. _om x = A.g i ( 1st ` y ) ) } ) = ( ( Fmla ` N ) u. { x | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) )
102 1 101 eqtrd 
 |-  ( N e. _om -> ( Fmla ` suc N ) = ( ( Fmla ` N ) u. { x | E. u e. ( Fmla ` N ) ( E. v e. ( Fmla ` N ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) )