Metamath Proof Explorer

Theorem fmlaomn0

Description: The empty set is not a Godel formula of any height. (Contributed by AV, 21-Oct-2023)

Ref Expression
Assertion fmlaomn0 
|- ( N e. _om -> (/) e/ ( Fmla ` N ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( x = (/) -> ( Fmla ` x ) = ( Fmla ` (/) ) )
2 1 eleq2d 
 |-  ( x = (/) -> ( (/) e. ( Fmla ` x ) <-> (/) e. ( Fmla ` (/) ) ) )
3 2 notbid 
 |-  ( x = (/) -> ( -. (/) e. ( Fmla ` x ) <-> -. (/) e. ( Fmla ` (/) ) ) )
4 fveq2 
 |-  ( x = y -> ( Fmla ` x ) = ( Fmla ` y ) )
5 4 eleq2d 
 |-  ( x = y -> ( (/) e. ( Fmla ` x ) <-> (/) e. ( Fmla ` y ) ) )
6 5 notbid 
 |-  ( x = y -> ( -. (/) e. ( Fmla ` x ) <-> -. (/) e. ( Fmla ` y ) ) )
7 fveq2 
 |-  ( x = suc y -> ( Fmla ` x ) = ( Fmla ` suc y ) )
8 7 eleq2d 
 |-  ( x = suc y -> ( (/) e. ( Fmla ` x ) <-> (/) e. ( Fmla ` suc y ) ) )
9 8 notbid 
 |-  ( x = suc y -> ( -. (/) e. ( Fmla ` x ) <-> -. (/) e. ( Fmla ` suc y ) ) )
10 fveq2 
 |-  ( x = N -> ( Fmla ` x ) = ( Fmla ` N ) )
11 10 eleq2d 
 |-  ( x = N -> ( (/) e. ( Fmla ` x ) <-> (/) e. ( Fmla ` N ) ) )
12 11 notbid 
 |-  ( x = N -> ( -. (/) e. ( Fmla ` x ) <-> -. (/) e. ( Fmla ` N ) ) )
13 0ex 
 |-  (/) e. _V
14 opex 
 |-  <. i , j >. e. _V
15 13 14 pm3.2i 
 |-  ( (/) e. _V /\ <. i , j >. e. _V )
16 15 a1i 
 |-  ( ( i e. _om /\ j e. _om ) -> ( (/) e. _V /\ <. i , j >. e. _V ) )
17 necom 
 |-  ( (/) =/= <. (/) , <. i , j >. >. <-> <. (/) , <. i , j >. >. =/= (/) )
18 opnz 
 |-  ( <. (/) , <. i , j >. >. =/= (/) <-> ( (/) e. _V /\ <. i , j >. e. _V ) )
19 17 18 bitri 
 |-  ( (/) =/= <. (/) , <. i , j >. >. <-> ( (/) e. _V /\ <. i , j >. e. _V ) )
20 16 19 sylibr 
 |-  ( ( i e. _om /\ j e. _om ) -> (/) =/= <. (/) , <. i , j >. >. )
21 20 neneqd 
 |-  ( ( i e. _om /\ j e. _om ) -> -. (/) = <. (/) , <. i , j >. >. )
22 goel 
 |-  ( ( i e. _om /\ j e. _om ) -> ( i e.g j ) = <. (/) , <. i , j >. >. )
23 22 eqeq2d 
 |-  ( ( i e. _om /\ j e. _om ) -> ( (/) = ( i e.g j ) <-> (/) = <. (/) , <. i , j >. >. ) )
24 21 23 mtbird 
 |-  ( ( i e. _om /\ j e. _om ) -> -. (/) = ( i e.g j ) )
25 24 rgen2 
 |-  A. i e. _om A. j e. _om -. (/) = ( i e.g j )
26 ralnex2 
 |-  ( A. i e. _om A. j e. _om -. (/) = ( i e.g j ) <-> -. E. i e. _om E. j e. _om (/) = ( i e.g j ) )
27 25 26 mpbi 
 |-  -. E. i e. _om E. j e. _om (/) = ( i e.g j )
28 27 intnan 
 |-  -. ( (/) e. _V /\ E. i e. _om E. j e. _om (/) = ( i e.g j ) )
29 fmla0 
 |-  ( Fmla ` (/) ) = { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) }
30 29 eleq2i 
 |-  ( (/) e. ( Fmla ` (/) ) <-> (/) e. { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } )
31 eqeq1 
 |-  ( x = (/) -> ( x = ( i e.g j ) <-> (/) = ( i e.g j ) ) )
32 31 2rexbidv 
 |-  ( x = (/) -> ( E. i e. _om E. j e. _om x = ( i e.g j ) <-> E. i e. _om E. j e. _om (/) = ( i e.g j ) ) )
33 32 elrab 
 |-  ( (/) e. { x e. _V | E. i e. _om E. j e. _om x = ( i e.g j ) } <-> ( (/) e. _V /\ E. i e. _om E. j e. _om (/) = ( i e.g j ) ) )
34 30 33 bitri 
 |-  ( (/) e. ( Fmla ` (/) ) <-> ( (/) e. _V /\ E. i e. _om E. j e. _om (/) = ( i e.g j ) ) )
35 28 34 mtbir 
 |-  -. (/) e. ( Fmla ` (/) )
36 simpr 
 |-  ( ( y e. _om /\ -. (/) e. ( Fmla ` y ) ) -> -. (/) e. ( Fmla ` y ) )
37 1oex 
 |-  1o e. _V
38 opex 
 |-  <. u , v >. e. _V
39 37 38 opnzi 
 |-  <. 1o , <. u , v >. >. =/= (/)
40 39 nesymi 
 |-  -. (/) = <. 1o , <. u , v >. >.
41 gonafv 
 |-  ( ( u e. ( Fmla ` y ) /\ v e. ( Fmla ` y ) ) -> ( u |g v ) = <. 1o , <. u , v >. >. )
42 41 adantll 
 |-  ( ( ( y e. _om /\ u e. ( Fmla ` y ) ) /\ v e. ( Fmla ` y ) ) -> ( u |g v ) = <. 1o , <. u , v >. >. )
43 42 eqeq2d 
 |-  ( ( ( y e. _om /\ u e. ( Fmla ` y ) ) /\ v e. ( Fmla ` y ) ) -> ( (/) = ( u |g v ) <-> (/) = <. 1o , <. u , v >. >. ) )
44 40 43 mtbiri 
 |-  ( ( ( y e. _om /\ u e. ( Fmla ` y ) ) /\ v e. ( Fmla ` y ) ) -> -. (/) = ( u |g v ) )
45 44 ralrimiva 
 |-  ( ( y e. _om /\ u e. ( Fmla ` y ) ) -> A. v e. ( Fmla ` y ) -. (/) = ( u |g v ) )
46 2oex 
 |-  2o e. _V
47 opex 
 |-  <. i , u >. e. _V
48 46 47 opnzi 
 |-  <. 2o , <. i , u >. >. =/= (/)
49 48 nesymi 
 |-  -. (/) = <. 2o , <. i , u >. >.
50 df-goal 
 |-  A.g i u = <. 2o , <. i , u >. >.
51 50 eqeq2i 
 |-  ( (/) = A.g i u <-> (/) = <. 2o , <. i , u >. >. )
52 49 51 mtbir 
 |-  -. (/) = A.g i u
53 52 a1i 
 |-  ( ( ( y e. _om /\ u e. ( Fmla ` y ) ) /\ i e. _om ) -> -. (/) = A.g i u )
54 53 ralrimiva 
 |-  ( ( y e. _om /\ u e. ( Fmla ` y ) ) -> A. i e. _om -. (/) = A.g i u )
55 45 54 jca 
 |-  ( ( y e. _om /\ u e. ( Fmla ` y ) ) -> ( A. v e. ( Fmla ` y ) -. (/) = ( u |g v ) /\ A. i e. _om -. (/) = A.g i u ) )
56 55 ralrimiva 
 |-  ( y e. _om -> A. u e. ( Fmla ` y ) ( A. v e. ( Fmla ` y ) -. (/) = ( u |g v ) /\ A. i e. _om -. (/) = A.g i u ) )
57 56 adantr 
 |-  ( ( y e. _om /\ -. (/) e. ( Fmla ` y ) ) -> A. u e. ( Fmla ` y ) ( A. v e. ( Fmla ` y ) -. (/) = ( u |g v ) /\ A. i e. _om -. (/) = A.g i u ) )
58 ralnex 
 |-  ( A. v e. ( Fmla ` y ) -. (/) = ( u |g v ) <-> -. E. v e. ( Fmla ` y ) (/) = ( u |g v ) )
59 ralnex 
 |-  ( A. i e. _om -. (/) = A.g i u <-> -. E. i e. _om (/) = A.g i u )
60 58 59 anbi12i 
 |-  ( ( A. v e. ( Fmla ` y ) -. (/) = ( u |g v ) /\ A. i e. _om -. (/) = A.g i u ) <-> ( -. E. v e. ( Fmla ` y ) (/) = ( u |g v ) /\ -. E. i e. _om (/) = A.g i u ) )
61 ioran 
 |-  ( -. ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) <-> ( -. E. v e. ( Fmla ` y ) (/) = ( u |g v ) /\ -. E. i e. _om (/) = A.g i u ) )
62 60 61 bitr4i 
 |-  ( ( A. v e. ( Fmla ` y ) -. (/) = ( u |g v ) /\ A. i e. _om -. (/) = A.g i u ) <-> -. ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) )
63 62 ralbii 
 |-  ( A. u e. ( Fmla ` y ) ( A. v e. ( Fmla ` y ) -. (/) = ( u |g v ) /\ A. i e. _om -. (/) = A.g i u ) <-> A. u e. ( Fmla ` y ) -. ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) )
64 ralnex 
 |-  ( A. u e. ( Fmla ` y ) -. ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) <-> -. E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) )
65 63 64 bitri 
 |-  ( A. u e. ( Fmla ` y ) ( A. v e. ( Fmla ` y ) -. (/) = ( u |g v ) /\ A. i e. _om -. (/) = A.g i u ) <-> -. E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) )
66 57 65 sylib 
 |-  ( ( y e. _om /\ -. (/) e. ( Fmla ` y ) ) -> -. E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) )
67 ioran 
 |-  ( -. ( (/) e. ( Fmla ` y ) \/ E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) ) <-> ( -. (/) e. ( Fmla ` y ) /\ -. E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) ) )
68 36 66 67 sylanbrc 
 |-  ( ( y e. _om /\ -. (/) e. ( Fmla ` y ) ) -> -. ( (/) e. ( Fmla ` y ) \/ E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) ) )
69 fmlasuc 
 |-  ( y e. _om -> ( Fmla ` suc y ) = ( ( Fmla ` y ) u. { x | E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) )
70 69 eleq2d 
 |-  ( y e. _om -> ( (/) e. ( Fmla ` suc y ) <-> (/) e. ( ( Fmla ` y ) u. { x | E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) ) )
71 elun 
 |-  ( (/) e. ( ( Fmla ` y ) u. { x | E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) <-> ( (/) e. ( Fmla ` y ) \/ (/) e. { x | E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) )
72 eqeq1 
 |-  ( x = (/) -> ( x = ( u |g v ) <-> (/) = ( u |g v ) ) )
73 72 rexbidv 
 |-  ( x = (/) -> ( E. v e. ( Fmla ` y ) x = ( u |g v ) <-> E. v e. ( Fmla ` y ) (/) = ( u |g v ) ) )
74 eqeq1 
 |-  ( x = (/) -> ( x = A.g i u <-> (/) = A.g i u ) )
75 74 rexbidv 
 |-  ( x = (/) -> ( E. i e. _om x = A.g i u <-> E. i e. _om (/) = A.g i u ) )
76 73 75 orbi12d 
 |-  ( x = (/) -> ( ( E. v e. ( Fmla ` y ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) <-> ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) ) )
77 76 rexbidv 
 |-  ( x = (/) -> ( E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) <-> E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) ) )
78 13 77 elab 
 |-  ( (/) e. { x | E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } <-> E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) )
79 78 orbi2i 
 |-  ( ( (/) e. ( Fmla ` y ) \/ (/) e. { x | E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) <-> ( (/) e. ( Fmla ` y ) \/ E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) ) )
80 71 79 bitri 
 |-  ( (/) e. ( ( Fmla ` y ) u. { x | E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) <-> ( (/) e. ( Fmla ` y ) \/ E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) ) )
81 70 80 bitrdi 
 |-  ( y e. _om -> ( (/) e. ( Fmla ` suc y ) <-> ( (/) e. ( Fmla ` y ) \/ E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) ) ) )
82 81 adantr 
 |-  ( ( y e. _om /\ -. (/) e. ( Fmla ` y ) ) -> ( (/) e. ( Fmla ` suc y ) <-> ( (/) e. ( Fmla ` y ) \/ E. u e. ( Fmla ` y ) ( E. v e. ( Fmla ` y ) (/) = ( u |g v ) \/ E. i e. _om (/) = A.g i u ) ) ) )
83 68 82 mtbird 
 |-  ( ( y e. _om /\ -. (/) e. ( Fmla ` y ) ) -> -. (/) e. ( Fmla ` suc y ) )
84 83 ex 
 |-  ( y e. _om -> ( -. (/) e. ( Fmla ` y ) -> -. (/) e. ( Fmla ` suc y ) ) )
85 3 6 9 12 35 84 finds 
 |-  ( N e. _om -> -. (/) e. ( Fmla ` N ) )
86 df-nel 
 |-  ( (/) e/ ( Fmla ` N ) <-> -. (/) e. ( Fmla ` N ) )
87 85 86 sylibr 
 |-  ( N e. _om -> (/) e/ ( Fmla ` N ) )