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 A → ¬ ∅ ∈ A ↔ ⋃ A / ∼ A = A

Proof

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