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 ¬ ∅ ∈ ( 𝐴 / )