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

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 ⊢ ( 𝑥 ∈ ω → ∅ ∉ ( Fmla ‘ 𝑥 ) )
2 df-nel ⊢ ( ∅ ∉ ( Fmla ‘ 𝑥 ) ↔ ¬ ∅ ∈ ( Fmla ‘ 𝑥 ) )
3 1 2 sylib ⊢ ( 𝑥 ∈ ω → ¬ ∅ ∈ ( Fmla ‘ 𝑥 ) )
4 3 nrex ⊢ ¬ ∃ 𝑥 ∈ ω ∅ ∈ ( Fmla ‘ 𝑥 )
5 df-nel ⊢ ( ∅ ∉ ( Fmla ‘ ω ) ↔ ¬ ∅ ∈ ( Fmla ‘ ω ) )
6 fmla ⊢ ( Fmla ‘ ω ) = ∪ 𝑥 ∈ ω ( Fmla ‘ 𝑥 )
7 6 eleq2i ⊢ ( ∅ ∈ ( Fmla ‘ ω ) ↔ ∅ ∈ ∪ 𝑥 ∈ ω ( Fmla ‘ 𝑥 ) )
8 eliun ⊢ ( ∅ ∈ ∪ 𝑥 ∈ ω ( Fmla ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ ω ∅ ∈ ( Fmla ‘ 𝑥 ) )
9 7 8 bitri ⊢ ( ∅ ∈ ( Fmla ‘ ω ) ↔ ∃ 𝑥 ∈ ω ∅ ∈ ( Fmla ‘ 𝑥 ) )
10 5 9 xchbinx ⊢ ( ∅ ∉ ( Fmla ‘ ω ) ↔ ¬ ∃ 𝑥 ∈ ω ∅ ∈ ( Fmla ‘ 𝑥 ) )
11 4 10 mpbir ⊢ ∅ ∉ ( Fmla ‘ ω )