Metamath Proof Explorer

Theorem 2goelgoanfmla1

Description: Two Godel-sets of membership combined with a Godel-set for NAND is a Godel formula of height 1. (Contributed by AV, 17-Nov-2023)

Ref Expression
Hypothesis satfv1fvfmla1.x 
|- X = ( ( I e.g J ) |g ( K e.g L ) )
Assertion 2goelgoanfmla1 
|- ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X e. ( Fmla ` 1o ) )

Proof

Step Hyp Ref Expression
1 satfv1fvfmla1.x 
 |-  X = ( ( I e.g J ) |g ( K e.g L ) )
2 simpll 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> I e. _om )
3 simplr 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> J e. _om )
4 simprl 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> K e. _om )
5 simprr 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> L e. _om )
6 oveq2 
 |-  ( n = L -> ( K e.g n ) = ( K e.g L ) )
7 6 oveq2d 
 |-  ( n = L -> ( ( I e.g J ) |g ( K e.g n ) ) = ( ( I e.g J ) |g ( K e.g L ) ) )
8 7 eqeq2d 
 |-  ( n = L -> ( X = ( ( I e.g J ) |g ( K e.g n ) ) <-> X = ( ( I e.g J ) |g ( K e.g L ) ) ) )
9 8 adantl 
 |-  ( ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) /\ n = L ) -> ( X = ( ( I e.g J ) |g ( K e.g n ) ) <-> X = ( ( I e.g J ) |g ( K e.g L ) ) ) )
10 1 a1i 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X = ( ( I e.g J ) |g ( K e.g L ) ) )
11 5 9 10 rspcedvd 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) )
12 11 orcd 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) \/ X = A.g K ( I e.g J ) ) )
13 oveq1 
 |-  ( i = I -> ( i e.g j ) = ( I e.g j ) )
14 13 oveq1d 
 |-  ( i = I -> ( ( i e.g j ) |g ( k e.g n ) ) = ( ( I e.g j ) |g ( k e.g n ) ) )
15 14 eqeq2d 
 |-  ( i = I -> ( X = ( ( i e.g j ) |g ( k e.g n ) ) <-> X = ( ( I e.g j ) |g ( k e.g n ) ) ) )
16 15 rexbidv 
 |-  ( i = I -> ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) <-> E. n e. _om X = ( ( I e.g j ) |g ( k e.g n ) ) ) )
17 eqidd 
 |-  ( i = I -> k = k )
18 17 13 goaleq12d 
 |-  ( i = I -> A.g k ( i e.g j ) = A.g k ( I e.g j ) )
19 18 eqeq2d 
 |-  ( i = I -> ( X = A.g k ( i e.g j ) <-> X = A.g k ( I e.g j ) ) )
20 16 19 orbi12d 
 |-  ( i = I -> ( ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) <-> ( E. n e. _om X = ( ( I e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( I e.g j ) ) ) )
21 oveq2 
 |-  ( j = J -> ( I e.g j ) = ( I e.g J ) )
22 21 oveq1d 
 |-  ( j = J -> ( ( I e.g j ) |g ( k e.g n ) ) = ( ( I e.g J ) |g ( k e.g n ) ) )
23 22 eqeq2d 
 |-  ( j = J -> ( X = ( ( I e.g j ) |g ( k e.g n ) ) <-> X = ( ( I e.g J ) |g ( k e.g n ) ) ) )
24 23 rexbidv 
 |-  ( j = J -> ( E. n e. _om X = ( ( I e.g j ) |g ( k e.g n ) ) <-> E. n e. _om X = ( ( I e.g J ) |g ( k e.g n ) ) ) )
25 eqidd 
 |-  ( j = J -> k = k )
26 25 21 goaleq12d 
 |-  ( j = J -> A.g k ( I e.g j ) = A.g k ( I e.g J ) )
27 26 eqeq2d 
 |-  ( j = J -> ( X = A.g k ( I e.g j ) <-> X = A.g k ( I e.g J ) ) )
28 24 27 orbi12d 
 |-  ( j = J -> ( ( E. n e. _om X = ( ( I e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( I e.g j ) ) <-> ( E. n e. _om X = ( ( I e.g J ) |g ( k e.g n ) ) \/ X = A.g k ( I e.g J ) ) ) )
29 oveq1 
 |-  ( k = K -> ( k e.g n ) = ( K e.g n ) )
30 29 oveq2d 
 |-  ( k = K -> ( ( I e.g J ) |g ( k e.g n ) ) = ( ( I e.g J ) |g ( K e.g n ) ) )
31 30 eqeq2d 
 |-  ( k = K -> ( X = ( ( I e.g J ) |g ( k e.g n ) ) <-> X = ( ( I e.g J ) |g ( K e.g n ) ) ) )
32 31 rexbidv 
 |-  ( k = K -> ( E. n e. _om X = ( ( I e.g J ) |g ( k e.g n ) ) <-> E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) ) )
33 id 
 |-  ( k = K -> k = K )
34 eqidd 
 |-  ( k = K -> ( I e.g J ) = ( I e.g J ) )
35 33 34 goaleq12d 
 |-  ( k = K -> A.g k ( I e.g J ) = A.g K ( I e.g J ) )
36 35 eqeq2d 
 |-  ( k = K -> ( X = A.g k ( I e.g J ) <-> X = A.g K ( I e.g J ) ) )
37 32 36 orbi12d 
 |-  ( k = K -> ( ( E. n e. _om X = ( ( I e.g J ) |g ( k e.g n ) ) \/ X = A.g k ( I e.g J ) ) <-> ( E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) \/ X = A.g K ( I e.g J ) ) ) )
38 20 28 37 rspc3ev 
 |-  ( ( ( I e. _om /\ J e. _om /\ K e. _om ) /\ ( E. n e. _om X = ( ( I e.g J ) |g ( K e.g n ) ) \/ X = A.g K ( I e.g J ) ) ) -> E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) )
39 2 3 4 12 38 syl31anc 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) )
40 1 ovexi 
 |-  X e. _V
41 eqeq1 
 |-  ( x = X -> ( x = ( ( i e.g j ) |g ( k e.g n ) ) <-> X = ( ( i e.g j ) |g ( k e.g n ) ) ) )
42 41 rexbidv 
 |-  ( x = X -> ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) <-> E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) ) )
43 eqeq1 
 |-  ( x = X -> ( x = A.g k ( i e.g j ) <-> X = A.g k ( i e.g j ) ) )
44 42 43 orbi12d 
 |-  ( x = X -> ( ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) <-> ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) ) )
45 44 rexbidv 
 |-  ( x = X -> ( E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) <-> E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) ) )
46 45 2rexbidv 
 |-  ( x = X -> ( E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) <-> E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) ) )
47 40 46 elab 
 |-  ( X e. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } <-> E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om X = ( ( i e.g j ) |g ( k e.g n ) ) \/ X = A.g k ( i e.g j ) ) )
48 39 47 sylibr 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X e. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } )
49 48 olcd 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> ( X e. ( { (/) } X. ( _om X. _om ) ) \/ X e. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) )
50 elun 
 |-  ( X e. ( ( { (/) } X. ( _om X. _om ) ) u. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) <-> ( X e. ( { (/) } X. ( _om X. _om ) ) \/ X e. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) )
51 49 50 sylibr 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X e. ( ( { (/) } X. ( _om X. _om ) ) u. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } ) )
52 fmla1 
 |-  ( Fmla ` 1o ) = ( ( { (/) } X. ( _om X. _om ) ) u. { x | E. i e. _om E. j e. _om E. k e. _om ( E. n e. _om x = ( ( i e.g j ) |g ( k e.g n ) ) \/ x = A.g k ( i e.g j ) ) } )
53 51 52 eleqtrrdi 
 |-  ( ( ( I e. _om /\ J e. _om ) /\ ( K e. _om /\ L e. _om ) ) -> X e. ( Fmla ` 1o ) )