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

Metamath Proof Explorer

Theorem prtlem400

Description: Lemma for prter2 and also a property of partitions . (Contributed by Rodolfo Medina, 15-Oct-2010) (Revised by Mario Carneiro, 12-Aug-2015)

		Ref	Expression
	Hypothesis	prtlem13.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
	Assertion	prtlem400	⊢ ¬ ∅ ∈ ( ∪ 𝐴 / ∼ )

Proof

Step	Hyp	Ref	Expression
1		prtlem13.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑥 ∈ 𝑢 ∧ 𝑦 ∈ 𝑢 ) }
2		neirr	⊢ ¬ ∅ ≠ ∅
3	1	prtlem16	⊢ dom ∼ = ∪ 𝐴
4		elqsn0	⊢ ( ( dom ∼ = ∪ 𝐴 ∧ ∅ ∈ ( ∪ 𝐴 / ∼ ) ) → ∅ ≠ ∅ )
5	3 4	mpan	⊢ ( ∅ ∈ ( ∪ 𝐴 / ∼ ) → ∅ ≠ ∅ )
6	2 5	mto	⊢ ¬ ∅ ∈ ( ∪ 𝐴 / ∼ )