Metamath Proof Explorer

Theorem disji2

Description: Property of a disjoint collection: if B ( X ) = C and B ( Y ) = D , and X =/= Y , then C and D are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Hypotheses disji.1 
|- ( x = X -> B = C )
disji.2 
|- ( x = Y -> B = D )
Assertion disji2 
|- ( ( Disj_ x e. A B /\ ( X e. A /\ Y e. A ) /\ X =/= Y ) -> ( C i^i D ) = (/) )

Proof

Step Hyp Ref Expression
1 disji.1 
 |-  ( x = X -> B = C )
2 disji.2 
 |-  ( x = Y -> B = D )
3 df-ne 
 |-  ( X =/= Y <-> -. X = Y )
4 disjors 
 |-  ( Disj_ x e. A B <-> A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) )
5 eqeq1 
 |-  ( y = X -> ( y = z <-> X = z ) )
6 nfcv 
 |-  F/_ x X
7 nfcv 
 |-  F/_ x C
8 6 7 1 csbhypf 
 |-  ( y = X -> [_ y / x ]_ B = C )
9 8 ineq1d 
 |-  ( y = X -> ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = ( C i^i [_ z / x ]_ B ) )
10 9 eqeq1d 
 |-  ( y = X -> ( ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) <-> ( C i^i [_ z / x ]_ B ) = (/) ) )
11 5 10 orbi12d 
 |-  ( y = X -> ( ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) <-> ( X = z \/ ( C i^i [_ z / x ]_ B ) = (/) ) ) )
12 eqeq2 
 |-  ( z = Y -> ( X = z <-> X = Y ) )
13 nfcv 
 |-  F/_ x Y
14 nfcv 
 |-  F/_ x D
15 13 14 2 csbhypf 
 |-  ( z = Y -> [_ z / x ]_ B = D )
16 15 ineq2d 
 |-  ( z = Y -> ( C i^i [_ z / x ]_ B ) = ( C i^i D ) )
17 16 eqeq1d 
 |-  ( z = Y -> ( ( C i^i [_ z / x ]_ B ) = (/) <-> ( C i^i D ) = (/) ) )
18 12 17 orbi12d 
 |-  ( z = Y -> ( ( X = z \/ ( C i^i [_ z / x ]_ B ) = (/) ) <-> ( X = Y \/ ( C i^i D ) = (/) ) ) )
19 11 18 rspc2v 
 |-  ( ( X e. A /\ Y e. A ) -> ( A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) -> ( X = Y \/ ( C i^i D ) = (/) ) ) )
20 4 19 syl5bi 
 |-  ( ( X e. A /\ Y e. A ) -> ( Disj_ x e. A B -> ( X = Y \/ ( C i^i D ) = (/) ) ) )
21 20 impcom 
 |-  ( ( Disj_ x e. A B /\ ( X e. A /\ Y e. A ) ) -> ( X = Y \/ ( C i^i D ) = (/) ) )
22 21 ord 
 |-  ( ( Disj_ x e. A B /\ ( X e. A /\ Y e. A ) ) -> ( -. X = Y -> ( C i^i D ) = (/) ) )
23 3 22 syl5bi 
 |-  ( ( Disj_ x e. A B /\ ( X e. A /\ Y e. A ) ) -> ( X =/= Y -> ( C i^i D ) = (/) ) )
24 23 3impia 
 |-  ( ( Disj_ x e. A B /\ ( X e. A /\ Y e. A ) /\ X =/= Y ) -> ( C i^i D ) = (/) )