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 ‘ ω )