Metamath Proof Explorer
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 |
⊢ ¬ ∅ ∈ ( ∪ 𝐴 / ∼ ) |