Metamath Proof Explorer


Theorem iota0ndef

Description: Example for an undefined iota being the empty 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). (Contributed by AV, 24-Aug-2022)

Ref Expression
Assertion iota0ndef ( ℩ 𝑥𝑦 𝑦𝑥 ) = ∅

Proof

Step Hyp Ref Expression
1 nalset ¬ ∃ 𝑥𝑦 𝑦𝑥
2 1 intnanr ¬ ( ∃ 𝑥𝑦 𝑦𝑥 ∧ ∃* 𝑥𝑦 𝑦𝑥 )
3 df-eu ( ∃! 𝑥𝑦 𝑦𝑥 ↔ ( ∃ 𝑥𝑦 𝑦𝑥 ∧ ∃* 𝑥𝑦 𝑦𝑥 ) )
4 2 3 mtbir ¬ ∃! 𝑥𝑦 𝑦𝑥
5 iotanul ( ¬ ∃! 𝑥𝑦 𝑦𝑥 → ( ℩ 𝑥𝑦 𝑦𝑥 ) = ∅ )
6 4 5 ax-mp ( ℩ 𝑥𝑦 𝑦𝑥 ) = ∅