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 ) = (/) )