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 ‘ ∅ ) ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = ∅

Proof

Step Hyp Ref Expression
1 fmla0 ( Fmla ‘ ∅ ) = { 𝑥 ∈ V ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) }
2 rabab { 𝑥 ∈ V ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) } = { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) }
3 1 2 eqtri ( Fmla ‘ ∅ ) = { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) }
4 3 ineq1i ( ( Fmla ‘ ∅ ) ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = ( { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) } ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } )
5 inab ( { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) } ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = { 𝑥 ∣ ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) ∧ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) }
6 goel ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑗𝑔 𝑘 ) = ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ )
7 6 eqeq2d ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗𝑔 𝑘 ) ↔ 𝑥 = ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ ) )
8 1n0 1o ≠ ∅
9 8 nesymi ¬ ∅ = 1o
10 9 intnanr ¬ ( ∅ = 1o ∧ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ )
11 gonafv ( ( 𝑢 ∈ V ∧ 𝑣 ∈ V ) → ( 𝑢𝑔 𝑣 ) = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ )
12 11 el2v ( 𝑢𝑔 𝑣 ) = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩
13 12 eqeq2i ( ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ( 𝑢𝑔 𝑣 ) ↔ ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ )
14 0ex ∅ ∈ V
15 opex 𝑗 , 𝑘 ⟩ ∈ V
16 14 15 opth ( ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ⟨ 1o , ⟨ 𝑢 , 𝑣 ⟩ ⟩ ↔ ( ∅ = 1o ∧ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) )
17 13 16 bitri ( ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ( 𝑢𝑔 𝑣 ) ↔ ( ∅ = 1o ∧ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑢 , 𝑣 ⟩ ) )
18 10 17 mtbir ¬ ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ( 𝑢𝑔 𝑣 )
19 eqeq1 ( 𝑥 = ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ → ( 𝑥 = ( 𝑢𝑔 𝑣 ) ↔ ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ( 𝑢𝑔 𝑣 ) ) )
20 18 19 mtbiri ( 𝑥 = ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ → ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) )
21 7 20 syl6bi ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗𝑔 𝑘 ) → ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) ) )
22 21 imp ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) → ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) )
23 22 adantr ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) )
24 23 ralrimivw ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) )
25 2on0 2o ≠ ∅
26 25 nesymi ¬ ∅ = 2o
27 26 orci ( ¬ ∅ = 2o ∨ ¬ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ )
28 14 15 opth ( ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ ↔ ( ∅ = 2o ∧ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ ) )
29 28 notbii ( ¬ ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ ↔ ¬ ( ∅ = 2o ∧ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ ) )
30 ianor ( ¬ ( ∅ = 2o ∧ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ ) ↔ ( ¬ ∅ = 2o ∨ ¬ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ ) )
31 29 30 bitri ( ¬ ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ ↔ ( ¬ ∅ = 2o ∨ ¬ ⟨ 𝑗 , 𝑘 ⟩ = ⟨ 𝑖 , 𝑢 ⟩ ) )
32 27 31 mpbir ¬ ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩
33 eqeq1 ( 𝑥 = ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ → ( 𝑥 = ∀𝑔 𝑖 𝑢 ↔ ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ∀𝑔 𝑖 𝑢 ) )
34 df-goal 𝑔 𝑖 𝑢 = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩
35 34 eqeq2i ( ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ∀𝑔 𝑖 𝑢 ↔ ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ )
36 33 35 bitrdi ( 𝑥 = ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ → ( 𝑥 = ∀𝑔 𝑖 𝑢 ↔ ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ = ⟨ 2o , ⟨ 𝑖 , 𝑢 ⟩ ⟩ ) )
37 32 36 mtbiri ( 𝑥 = ⟨ ∅ , ⟨ 𝑗 , 𝑘 ⟩ ⟩ → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 )
38 7 37 syl6bi ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗𝑔 𝑘 ) → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) )
39 38 imp ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 )
40 39 adantr ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 )
41 40 adantr ( ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) ∧ 𝑖 ∈ ω ) → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 )
42 41 ralrimiva ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 )
43 24 42 jca ( ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) ∧ 𝑢 ∈ ( Fmla ‘ ∅ ) ) → ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) )
44 43 ralrimiva ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) → ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) )
45 ralnex ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) ↔ ¬ ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) )
46 ralnex ( ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ↔ ¬ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 )
47 45 46 anbi12i ( ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ¬ ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∧ ¬ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
48 ioran ( ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ( ¬ ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∧ ¬ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
49 47 48 bitr4i ( ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
50 49 ralbii ( ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
51 ralnex ( ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ¬ ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
52 50 51 bitri ( ∀ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∀ 𝑣 ∈ ( Fmla ‘ ∅ ) ¬ 𝑥 = ( 𝑢𝑔 𝑣 ) ∧ ∀ 𝑖 ∈ ω ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) ↔ ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
53 44 52 sylib ( ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) ∧ 𝑥 = ( 𝑗𝑔 𝑘 ) ) → ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
54 53 ex ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗𝑔 𝑘 ) → ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) )
55 54 rexlimdva ( 𝑗 ∈ ω → ( ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) → ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) )
56 55 rexlimiv ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) → ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
57 56 imori ( ¬ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) ∨ ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
58 ianor ( ¬ ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) ∧ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) ↔ ( ¬ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) ∨ ¬ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) )
59 57 58 mpbir ¬ ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) ∧ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) )
60 59 abf { 𝑥 ∣ ( ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) ∧ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) ) } = ∅
61 5 60 eqtri ( { 𝑥 ∣ ∃ 𝑗 ∈ ω ∃ 𝑘 ∈ ω 𝑥 = ( 𝑗𝑔 𝑘 ) } ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = ∅
62 4 61 eqtri ( ( Fmla ‘ ∅ ) ∩ { 𝑥 ∣ ∃ 𝑢 ∈ ( Fmla ‘ ∅ ) ( ∃ 𝑣 ∈ ( Fmla ‘ ∅ ) 𝑥 = ( 𝑢𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = ∅