Metamath Proof Explorer

Theorem fmla0disjsuc

Description: The set of valid Godel formulas of height 0 is disjoint with the formulas constructed from Godel-sets for the Sheffer stroke NAND and Godel-set of universal quantification. (Contributed by AV, 20-Oct-2023)

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

Proof

Step Hyp Ref Expression
1 fmla0 
 |-  ( Fmla ` (/) ) = { x e. _V | E. j e. _om E. k e. _om x = ( j e.g k ) }
2 rabab 
 |-  { x e. _V | E. j e. _om E. k e. _om x = ( j e.g k ) } = { x | E. j e. _om E. k e. _om x = ( j e.g k ) }
3 1 2 eqtri 
 |-  ( Fmla ` (/) ) = { x | E. j e. _om E. k e. _om x = ( j e.g k ) }
4 3 ineq1i 
 |-  ( ( Fmla ` (/) ) i^i { x | E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) = ( { x | E. j e. _om E. k e. _om x = ( j e.g k ) } i^i { x | E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } )
5 inab 
 |-  ( { x | E. j e. _om E. k e. _om x = ( j e.g k ) } i^i { x | E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) = { x | ( E. j e. _om E. k e. _om x = ( j e.g k ) /\ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) }
6 goel 
 |-  ( ( j e. _om /\ k e. _om ) -> ( j e.g k ) = <. (/) , <. j , k >. >. )
7 6 eqeq2d 
 |-  ( ( j e. _om /\ k e. _om ) -> ( x = ( j e.g k ) <-> x = <. (/) , <. j , k >. >. ) )
8 1n0 
 |-  1o =/= (/)
9 8 nesymi 
 |-  -. (/) = 1o
10 9 intnanr 
 |-  -. ( (/) = 1o /\ <. j , k >. = <. u , v >. )
11 gonafv 
 |-  ( ( u e. _V /\ v e. _V ) -> ( u |g v ) = <. 1o , <. u , v >. >. )
12 11 el2v 
 |-  ( u |g v ) = <. 1o , <. u , v >. >.
13 12 eqeq2i 
 |-  ( <. (/) , <. j , k >. >. = ( u |g v ) <-> <. (/) , <. j , k >. >. = <. 1o , <. u , v >. >. )
14 0ex 
 |-  (/) e. _V
15 opex 
 |-  <. j , k >. e. _V
16 14 15 opth 
 |-  ( <. (/) , <. j , k >. >. = <. 1o , <. u , v >. >. <-> ( (/) = 1o /\ <. j , k >. = <. u , v >. ) )
17 13 16 bitri 
 |-  ( <. (/) , <. j , k >. >. = ( u |g v ) <-> ( (/) = 1o /\ <. j , k >. = <. u , v >. ) )
18 10 17 mtbir 
 |-  -. <. (/) , <. j , k >. >. = ( u |g v )
19 eqeq1 
 |-  ( x = <. (/) , <. j , k >. >. -> ( x = ( u |g v ) <-> <. (/) , <. j , k >. >. = ( u |g v ) ) )
20 18 19 mtbiri 
 |-  ( x = <. (/) , <. j , k >. >. -> -. x = ( u |g v ) )
21 7 20 syl6bi 
 |-  ( ( j e. _om /\ k e. _om ) -> ( x = ( j e.g k ) -> -. x = ( u |g v ) ) )
22 21 imp 
 |-  ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) -> -. x = ( u |g v ) )
23 22 adantr 
 |-  ( ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) /\ u e. ( Fmla ` (/) ) ) -> -. x = ( u |g v ) )
24 23 ralrimivw 
 |-  ( ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) /\ u e. ( Fmla ` (/) ) ) -> A. v e. ( Fmla ` (/) ) -. x = ( u |g v ) )
25 2on0 
 |-  2o =/= (/)
26 25 nesymi 
 |-  -. (/) = 2o
27 26 orci 
 |-  ( -. (/) = 2o \/ -. <. j , k >. = <. i , u >. )
28 14 15 opth 
 |-  ( <. (/) , <. j , k >. >. = <. 2o , <. i , u >. >. <-> ( (/) = 2o /\ <. j , k >. = <. i , u >. ) )
29 28 notbii 
 |-  ( -. <. (/) , <. j , k >. >. = <. 2o , <. i , u >. >. <-> -. ( (/) = 2o /\ <. j , k >. = <. i , u >. ) )
30 ianor 
 |-  ( -. ( (/) = 2o /\ <. j , k >. = <. i , u >. ) <-> ( -. (/) = 2o \/ -. <. j , k >. = <. i , u >. ) )
31 29 30 bitri 
 |-  ( -. <. (/) , <. j , k >. >. = <. 2o , <. i , u >. >. <-> ( -. (/) = 2o \/ -. <. j , k >. = <. i , u >. ) )
32 27 31 mpbir 
 |-  -. <. (/) , <. j , k >. >. = <. 2o , <. i , u >. >.
33 eqeq1 
 |-  ( x = <. (/) , <. j , k >. >. -> ( x = A.g i u <-> <. (/) , <. j , k >. >. = A.g i u ) )
34 df-goal 
 |-  A.g i u = <. 2o , <. i , u >. >.
35 34 eqeq2i 
 |-  ( <. (/) , <. j , k >. >. = A.g i u <-> <. (/) , <. j , k >. >. = <. 2o , <. i , u >. >. )
36 33 35 bitrdi 
 |-  ( x = <. (/) , <. j , k >. >. -> ( x = A.g i u <-> <. (/) , <. j , k >. >. = <. 2o , <. i , u >. >. ) )
37 32 36 mtbiri 
 |-  ( x = <. (/) , <. j , k >. >. -> -. x = A.g i u )
38 7 37 syl6bi 
 |-  ( ( j e. _om /\ k e. _om ) -> ( x = ( j e.g k ) -> -. x = A.g i u ) )
39 38 imp 
 |-  ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) -> -. x = A.g i u )
40 39 adantr 
 |-  ( ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) /\ u e. ( Fmla ` (/) ) ) -> -. x = A.g i u )
41 40 adantr 
 |-  ( ( ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) /\ u e. ( Fmla ` (/) ) ) /\ i e. _om ) -> -. x = A.g i u )
42 41 ralrimiva 
 |-  ( ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) /\ u e. ( Fmla ` (/) ) ) -> A. i e. _om -. x = A.g i u )
43 24 42 jca 
 |-  ( ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) /\ u e. ( Fmla ` (/) ) ) -> ( A. v e. ( Fmla ` (/) ) -. x = ( u |g v ) /\ A. i e. _om -. x = A.g i u ) )
44 43 ralrimiva 
 |-  ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) -> A. u e. ( Fmla ` (/) ) ( A. v e. ( Fmla ` (/) ) -. x = ( u |g v ) /\ A. i e. _om -. x = A.g i u ) )
45 ralnex 
 |-  ( A. v e. ( Fmla ` (/) ) -. x = ( u |g v ) <-> -. E. v e. ( Fmla ` (/) ) x = ( u |g v ) )
46 ralnex 
 |-  ( A. i e. _om -. x = A.g i u <-> -. E. i e. _om x = A.g i u )
47 45 46 anbi12i 
 |-  ( ( A. v e. ( Fmla ` (/) ) -. x = ( u |g v ) /\ A. i e. _om -. x = A.g i u ) <-> ( -. E. v e. ( Fmla ` (/) ) x = ( u |g v ) /\ -. E. i e. _om x = A.g i u ) )
48 ioran 
 |-  ( -. ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) <-> ( -. E. v e. ( Fmla ` (/) ) x = ( u |g v ) /\ -. E. i e. _om x = A.g i u ) )
49 47 48 bitr4i 
 |-  ( ( A. v e. ( Fmla ` (/) ) -. x = ( u |g v ) /\ A. i e. _om -. x = A.g i u ) <-> -. ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) )
50 49 ralbii 
 |-  ( A. u e. ( Fmla ` (/) ) ( A. v e. ( Fmla ` (/) ) -. x = ( u |g v ) /\ A. i e. _om -. x = A.g i u ) <-> A. u e. ( Fmla ` (/) ) -. ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) )
51 ralnex 
 |-  ( A. u e. ( Fmla ` (/) ) -. ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) <-> -. E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) )
52 50 51 bitri 
 |-  ( A. u e. ( Fmla ` (/) ) ( A. v e. ( Fmla ` (/) ) -. x = ( u |g v ) /\ A. i e. _om -. x = A.g i u ) <-> -. E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) )
53 44 52 sylib 
 |-  ( ( ( j e. _om /\ k e. _om ) /\ x = ( j e.g k ) ) -> -. E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) )
54 53 ex 
 |-  ( ( j e. _om /\ k e. _om ) -> ( x = ( j e.g k ) -> -. E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) )
55 54 rexlimdva 
 |-  ( j e. _om -> ( E. k e. _om x = ( j e.g k ) -> -. E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) )
56 55 rexlimiv 
 |-  ( E. j e. _om E. k e. _om x = ( j e.g k ) -> -. E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) )
57 56 imori 
 |-  ( -. E. j e. _om E. k e. _om x = ( j e.g k ) \/ -. E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) )
58 ianor 
 |-  ( -. ( E. j e. _om E. k e. _om x = ( j e.g k ) /\ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) <-> ( -. E. j e. _om E. k e. _om x = ( j e.g k ) \/ -. E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) )
59 57 58 mpbir 
 |-  -. ( E. j e. _om E. k e. _om x = ( j e.g k ) /\ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) )
60 59 abf 
 |-  { x | ( E. j e. _om E. k e. _om x = ( j e.g k ) /\ E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) ) } = (/)
61 5 60 eqtri 
 |-  ( { x | E. j e. _om E. k e. _om x = ( j e.g k ) } i^i { x | E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) = (/)
62 4 61 eqtri 
 |-  ( ( Fmla ` (/) ) i^i { x | E. u e. ( Fmla ` (/) ) ( E. v e. ( Fmla ` (/) ) x = ( u |g v ) \/ E. i e. _om x = A.g i u ) } ) = (/)