Theorem aiota0ndef

Description: Example for an undefined alternate iota being no set, i.e., A. y y e. x is a wff not satisfied by a (unique) value x (there is no set, and therefore certainly no unique set, which contains every set). This is different from iota0ndef , where the iota still is a set (the empty set). (Contributed by AV, 25-Aug-2022)

	Ref	Expression
Assertion	aiota0ndef	⊢ ( ℩' 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) ∉ V

Proof

Step	Hyp	Ref	Expression
1		nalset	⊢ ¬ ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥
2	1	intnanr	⊢ ¬ ( ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ∧ ∃* 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 )
3		df-eu	⊢ ( ∃! 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ↔ ( ∃ 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ∧ ∃* 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) )
4	2 3	mtbir	⊢ ¬ ∃! 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥
5		df-nel	⊢ ( ( ℩' 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) ∉ V ↔ ¬ ( ℩' 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) ∈ V )
6		aiotaexb	⊢ ( ∃! 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ↔ ( ℩' 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) ∈ V )
7	5 6	xchbinxr	⊢ ( ( ℩' 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) ∉ V ↔ ¬ ∃! 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 )
8	4 7	mpbir	⊢ ( ℩' 𝑥 ∀ 𝑦 𝑦 ∈ 𝑥 ) ∉ V