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⁡ω