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 𝐴 → ( ¬ ∅ ∈ 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )