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

Metamath Proof Explorer

Theorem disjiunel

Description: A set of elements B of a disjoint set A is disjoint with another element of that set. (Contributed by Thierry Arnoux, 24-May-2020)

Ref Expression
Hypotheses disjiunel.1 
|- ( ph -> Disj_ x e. A B )
disjiunel.2 
|- ( x = Y -> B = D )
disjiunel.3 
|- ( ph -> E C_ A )
disjiunel.4 
|- ( ph -> Y e. ( A \ E ) )
Assertion disjiunel 
|- ( ph -> ( U_ x e. E B i^i D ) = (/) )

Proof

Step Hyp Ref Expression
1 disjiunel.1 
 |-  ( ph -> Disj_ x e. A B )
2 disjiunel.2 
 |-  ( x = Y -> B = D )
3 disjiunel.3 
 |-  ( ph -> E C_ A )
4 disjiunel.4 
 |-  ( ph -> Y e. ( A \ E ) )
5 4 eldifad 
 |-  ( ph -> Y e. A )
6 5 snssd 
 |-  ( ph -> { Y } C_ A )
7 3 6 unssd 
 |-  ( ph -> ( E u. { Y } ) C_ A )
8 disjss1 
 |-  ( ( E u. { Y } ) C_ A -> ( Disj_ x e. A B -> Disj_ x e. ( E u. { Y } ) B ) )
9 7 1 8 sylc 
 |-  ( ph -> Disj_ x e. ( E u. { Y } ) B )
10 4 eldifbd 
 |-  ( ph -> -. Y e. E )
11 2 disjunsn 
 |-  ( ( Y e. A /\ -. Y e. E ) -> ( Disj_ x e. ( E u. { Y } ) B <-> ( Disj_ x e. E B /\ ( U_ x e. E B i^i D ) = (/) ) ) )
12 5 10 11 syl2anc 
 |-  ( ph -> ( Disj_ x e. ( E u. { Y } ) B <-> ( Disj_ x e. E B /\ ( U_ x e. E B i^i D ) = (/) ) ) )
13 9 12 mpbid 
 |-  ( ph -> ( Disj_ x e. E B /\ ( U_ x e. E B i^i D ) = (/) ) )
14 13 simprd 
 |-  ( ph -> ( U_ x e. E B i^i D ) = (/) )