Metamath Proof Explorer

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 ⊢ ¬ ∃ x ∀ y y ∈ x
2 1 intnanr ⊢ ¬ ∃ x ∀ y y ∈ x ∧ ∃* x ∀ y y ∈ x
3 df-eu ⊢ ∃! x ∀ y y ∈ x ↔ ∃ x ∀ y y ∈ x ∧ ∃* x ∀ y y ∈ x
4 2 3 mtbir ⊢ ¬ ∃! x ∀ y y ∈ x
5 df-nel ⊢ ι ∉ V ↔ ¬ ι ∈ V
6 aiotaexb ⊢ ∃! x ∀ y y ∈ x ↔ ι ∈ V
7 5 6 xchbinxr ⊢ ι ∉ V ↔ ¬ ∃! x ∀ y y ∈ x
8 4 7 mpbir ⊢ ι ∉ V