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

Metamath Proof Explorer

Theorem disjun0

Description: Adding the empty element preserves disjointness. (Contributed by Thierry Arnoux, 30-May-2020)

Ref Expression
Assertion disjun0 ⊢ Disj x ∈ A x → Disj x ∈ A ∪ ∅ x

Proof

Step Hyp Ref Expression
1 snssi ⊢ ∅ ∈ A → ∅ ⊆ A
2 ssequn2 ⊢ ∅ ⊆ A ↔ A ∪ ∅ = A
3 1 2 sylib ⊢ ∅ ∈ A → A ∪ ∅ = A
4 3 disjeq1d ⊢ ∅ ∈ A → Disj x ∈ A ∪ ∅ x ↔ Disj x ∈ A x
5 4 biimparc ⊢ Disj x ∈ A x ∧ ∅ ∈ A → Disj x ∈ A ∪ ∅ x
6 simpl ⊢ Disj x ∈ A x ∧ ¬ ∅ ∈ A → Disj x ∈ A x
7 in0 ⊢ ⋃ x ∈ A x ∩ ∅ = ∅
8 7 a1i ⊢ Disj x ∈ A x ∧ ¬ ∅ ∈ A → ⋃ x ∈ A x ∩ ∅ = ∅
9 0ex ⊢ ∅ ∈ V
10 id ⊢ x = ∅ → x = ∅
11 10 disjunsn ⊢ ∅ ∈ V ∧ ¬ ∅ ∈ A → Disj x ∈ A ∪ ∅ x ↔ Disj x ∈ A x ∧ ⋃ x ∈ A x ∩ ∅ = ∅
12 9 11 mpan ⊢ ¬ ∅ ∈ A → Disj x ∈ A ∪ ∅ x ↔ Disj x ∈ A x ∧ ⋃ x ∈ A x ∩ ∅ = ∅
13 12 adantl ⊢ Disj x ∈ A x ∧ ¬ ∅ ∈ A → Disj x ∈ A ∪ ∅ x ↔ Disj x ∈ A x ∧ ⋃ x ∈ A x ∩ ∅ = ∅
14 6 8 13 mpbir2and ⊢ Disj x ∈ A x ∧ ¬ ∅ ∈ A → Disj x ∈ A ∪ ∅ x
15 5 14 pm2.61dan ⊢ Disj x ∈ A x → Disj x ∈ A ∪ ∅ x