This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrdi ⊢ ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) → ¬ 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ) )
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 biimtrdi ⊢ ( ( 𝑗 ∈ ω ∧ 𝑘 ∈ ω ) → ( 𝑥 = ( 𝑗 ∈𝑔 𝑘 ) → ¬ 𝑥 = ∀𝑔 𝑖 𝑢 ) )
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 ‘ ∅ ) 𝑥 = ( 𝑢 ⊼𝑔 𝑣 ) ∨ ∃ 𝑖 ∈ ω 𝑥 = ∀𝑔 𝑖 𝑢 ) } ) = ∅