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