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

Metamath Proof Explorer

Theorem eldisjn0el

Description: Special case of disjdmqseq (perhaps this is the closest theorem to the former prter2 ). (Contributed by Peter Mazsa, 26-Sep-2021)

Ref Expression
Assertion eldisjn0el ( ElDisj 𝐴 → ( ¬ ∅ ∈ 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 disjdmqseq ⊢ ( Disj ( ◡ E ↾ 𝐴 ) → ( ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 ↔ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) )
2 df-eldisj ⊢ ( ElDisj 𝐴 ↔ Disj ( ◡ E ↾ 𝐴 ) )
3 n0el3 ⊢ ( ¬ ∅ ∈ 𝐴 ↔ ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 )
4 dmqs1cosscnvepreseq ⊢ ( ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 )
5 4 bicomi ⊢ ( ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ↔ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 )
6 3 5 bibi12i ⊢ ( ( ¬ ∅ ∈ 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) ↔ ( ( dom ( ◡ E ↾ 𝐴 ) / ( ◡ E ↾ 𝐴 ) ) = 𝐴 ↔ ( dom ≀ ( ◡ E ↾ 𝐴 ) / ≀ ( ◡ E ↾ 𝐴 ) ) = 𝐴 ) )
7 1 2 6 3imtr4i ⊢ ( ElDisj 𝐴 → ( ¬ ∅ ∈ 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )