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

Metamath Proof Explorer

Theorem iotanul2

Description: Version of iotanul using df-iota instead of dfiota2 . (Contributed by SN, 6-Nov-2024)

Ref Expression
Assertion iotanul2 ( ¬ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∅ )

Proof

Step Hyp Ref Expression
1 df-iota ⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } }
2 n0 ⊢ ( ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ≠ ∅ ↔ ∃ 𝑣 𝑣 ∈ ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } )
3 eluni ⊢ ( 𝑣 ∈ ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ↔ ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ) )
4 vex ⊢ 𝑦 ∈ V
5 sneq ⊢ ( 𝑤 = 𝑦 → { 𝑤 } = { 𝑦 } )
6 5 eqeq2d ⊢ ( 𝑤 = 𝑦 → ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } ) )
7 4 6 elab ⊢ ( 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ↔ { 𝑥 ∣ 𝜑 } = { 𝑦 } )
8 7 biimpi ⊢ ( 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } → { 𝑥 ∣ 𝜑 } = { 𝑦 } )
9 8 adantl ⊢ ( ( 𝑣 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ) → { 𝑥 ∣ 𝜑 } = { 𝑦 } )
10 9 eximi ⊢ ( ∃ 𝑦 ( 𝑣 ∈ 𝑦 ∧ 𝑦 ∈ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ) → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
11 3 10 sylbi ⊢ ( 𝑣 ∈ ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
12 11 exlimiv ⊢ ( ∃ 𝑣 𝑣 ∈ ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
13 2 12 sylbi ⊢ ( ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } ≠ ∅ → ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } )
14 13 necon1bi ⊢ ( ¬ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ∪ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } = ∅ )
15 1 14 eqtrid ⊢ ( ¬ ∃ 𝑦 { 𝑥 ∣ 𝜑 } = { 𝑦 } → ( ℩ 𝑥 𝜑 ) = ∅ )