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 e. A x -> Disj_ x e. ( A u. { (/) } ) x )

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( (/) e. A -> { (/) } C_ A )
2 ssequn2 
 |-  ( { (/) } C_ A <-> ( A u. { (/) } ) = A )
3 1 2 sylib 
 |-  ( (/) e. A -> ( A u. { (/) } ) = A )
4 3 disjeq1d 
 |-  ( (/) e. A -> ( Disj_ x e. ( A u. { (/) } ) x <-> Disj_ x e. A x ) )
5 4 biimparc 
 |-  ( ( Disj_ x e. A x /\ (/) e. A ) -> Disj_ x e. ( A u. { (/) } ) x )
6 simpl 
 |-  ( ( Disj_ x e. A x /\ -. (/) e. A ) -> Disj_ x e. A x )
7 in0 
 |-  ( U_ x e. A x i^i (/) ) = (/)
8 7 a1i 
 |-  ( ( Disj_ x e. A x /\ -. (/) e. A ) -> ( U_ x e. A x i^i (/) ) = (/) )
9 0ex 
 |-  (/) e. _V
10 id 
 |-  ( x = (/) -> x = (/) )
11 10 disjunsn 
 |-  ( ( (/) e. _V /\ -. (/) e. A ) -> ( Disj_ x e. ( A u. { (/) } ) x <-> ( Disj_ x e. A x /\ ( U_ x e. A x i^i (/) ) = (/) ) ) )
12 9 11 mpan 
 |-  ( -. (/) e. A -> ( Disj_ x e. ( A u. { (/) } ) x <-> ( Disj_ x e. A x /\ ( U_ x e. A x i^i (/) ) = (/) ) ) )
13 12 adantl 
 |-  ( ( Disj_ x e. A x /\ -. (/) e. A ) -> ( Disj_ x e. ( A u. { (/) } ) x <-> ( Disj_ x e. A x /\ ( U_ x e. A x i^i (/) ) = (/) ) ) )
14 6 8 13 mpbir2and 
 |-  ( ( Disj_ x e. A x /\ -. (/) e. A ) -> Disj_ x e. ( A u. { (/) } ) x )
15 5 14 pm2.61dan 
 |-  ( Disj_ x e. A x -> Disj_ x e. ( A u. { (/) } ) x )