Metamath Proof Explorer

Theorem disjss3

Description: Expand a disjoint collection with any number of empty sets. (Contributed by Mario Carneiro, 15-Nov-2016)

Ref Expression
Assertion disjss3 
|- ( ( A C_ B /\ A. x e. ( B \ A ) C = (/) ) -> ( Disj_ x e. A C <-> Disj_ x e. B C ) )

Proof

Step Hyp Ref Expression
1 df-ral 
 |-  ( A. x e. ( B \ A ) C = (/) <-> A. x ( x e. ( B \ A ) -> C = (/) ) )
2 simprr 
 |-  ( ( ( x e. ( B \ A ) -> C = (/) ) /\ ( x e. B /\ y e. C ) ) -> y e. C )
3 n0i 
 |-  ( y e. C -> -. C = (/) )
4 2 3 syl 
 |-  ( ( ( x e. ( B \ A ) -> C = (/) ) /\ ( x e. B /\ y e. C ) ) -> -. C = (/) )
5 simpl 
 |-  ( ( x e. B /\ y e. C ) -> x e. B )
6 5 adantl 
 |-  ( ( ( x e. ( B \ A ) -> C = (/) ) /\ ( x e. B /\ y e. C ) ) -> x e. B )
7 eldif 
 |-  ( x e. ( B \ A ) <-> ( x e. B /\ -. x e. A ) )
8 simpl 
 |-  ( ( ( x e. ( B \ A ) -> C = (/) ) /\ ( x e. B /\ y e. C ) ) -> ( x e. ( B \ A ) -> C = (/) ) )
9 7 8 syl5bir 
 |-  ( ( ( x e. ( B \ A ) -> C = (/) ) /\ ( x e. B /\ y e. C ) ) -> ( ( x e. B /\ -. x e. A ) -> C = (/) ) )
10 6 9 mpand 
 |-  ( ( ( x e. ( B \ A ) -> C = (/) ) /\ ( x e. B /\ y e. C ) ) -> ( -. x e. A -> C = (/) ) )
11 4 10 mt3d 
 |-  ( ( ( x e. ( B \ A ) -> C = (/) ) /\ ( x e. B /\ y e. C ) ) -> x e. A )
12 11 2 jca 
 |-  ( ( ( x e. ( B \ A ) -> C = (/) ) /\ ( x e. B /\ y e. C ) ) -> ( x e. A /\ y e. C ) )
13 12 ex 
 |-  ( ( x e. ( B \ A ) -> C = (/) ) -> ( ( x e. B /\ y e. C ) -> ( x e. A /\ y e. C ) ) )
14 13 alimi 
 |-  ( A. x ( x e. ( B \ A ) -> C = (/) ) -> A. x ( ( x e. B /\ y e. C ) -> ( x e. A /\ y e. C ) ) )
15 1 14 sylbi 
 |-  ( A. x e. ( B \ A ) C = (/) -> A. x ( ( x e. B /\ y e. C ) -> ( x e. A /\ y e. C ) ) )
16 moim 
 |-  ( A. x ( ( x e. B /\ y e. C ) -> ( x e. A /\ y e. C ) ) -> ( E* x ( x e. A /\ y e. C ) -> E* x ( x e. B /\ y e. C ) ) )
17 15 16 syl 
 |-  ( A. x e. ( B \ A ) C = (/) -> ( E* x ( x e. A /\ y e. C ) -> E* x ( x e. B /\ y e. C ) ) )
18 17 alimdv 
 |-  ( A. x e. ( B \ A ) C = (/) -> ( A. y E* x ( x e. A /\ y e. C ) -> A. y E* x ( x e. B /\ y e. C ) ) )
19 dfdisj2 
 |-  ( Disj_ x e. A C <-> A. y E* x ( x e. A /\ y e. C ) )
20 dfdisj2 
 |-  ( Disj_ x e. B C <-> A. y E* x ( x e. B /\ y e. C ) )
21 18 19 20 3imtr4g 
 |-  ( A. x e. ( B \ A ) C = (/) -> ( Disj_ x e. A C -> Disj_ x e. B C ) )
22 21 adantl 
 |-  ( ( A C_ B /\ A. x e. ( B \ A ) C = (/) ) -> ( Disj_ x e. A C -> Disj_ x e. B C ) )
23 disjss1 
 |-  ( A C_ B -> ( Disj_ x e. B C -> Disj_ x e. A C ) )
24 23 adantr 
 |-  ( ( A C_ B /\ A. x e. ( B \ A ) C = (/) ) -> ( Disj_ x e. B C -> Disj_ x e. A C ) )
25 22 24 impbid 
 |-  ( ( A C_ B /\ A. x e. ( B \ A ) C = (/) ) -> ( Disj_ x e. A C <-> Disj_ x e. B C ) )