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 𝑥 ∈ 𝐴 𝑥 → Disj 𝑥 ∈ ( 𝐴 ∪ { ∅ } ) 𝑥 )

Proof

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