Metamath Proof Explorer

Theorem fmlan0

Description: The empty set is not a Godel formula. (Contributed by AV, 19-Nov-2023)

Ref Expression
Assertion fmlan0 ⊢ ∅ ∉ Fmla ⁡ ω

Proof

Step Hyp Ref Expression
1 fmlaomn0 ⊢ x ∈ ω → ∅ ∉ Fmla ⁡ x
2 df-nel ⊢ ∅ ∉ Fmla ⁡ x ↔ ¬ ∅ ∈ Fmla ⁡ x
3 1 2 sylib ⊢ x ∈ ω → ¬ ∅ ∈ Fmla ⁡ x
4 3 nrex ⊢ ¬ ∃ x ∈ ω ∅ ∈ Fmla ⁡ x
5 df-nel ⊢ ∅ ∉ Fmla ⁡ ω ↔ ¬ ∅ ∈ Fmla ⁡ ω
6 fmla ⊢ Fmla ⁡ ω = ⋃ x ∈ ω Fmla ⁡ x
7 6 eleq2i ⊢ ∅ ∈ Fmla ⁡ ω ↔ ∅ ∈ ⋃ x ∈ ω Fmla ⁡ x
8 eliun ⊢ ∅ ∈ ⋃ x ∈ ω Fmla ⁡ x ↔ ∃ x ∈ ω ∅ ∈ Fmla ⁡ x
9 7 8 bitri ⊢ ∅ ∈ Fmla ⁡ ω ↔ ∃ x ∈ ω ∅ ∈ Fmla ⁡ x
10 5 9 xchbinx ⊢ ∅ ∉ Fmla ⁡ ω ↔ ¬ ∃ x ∈ ω ∅ ∈ Fmla ⁡ x
11 4 10 mpbir ⊢ ∅ ∉ Fmla ⁡ ω