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 ) } ) = (/)