Metamath Proof Explorer

Theorem disji2f

Description: Property of a disjoint collection: if B ( x ) = C and B ( Y ) = D , and x =/= Y , then B and C are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016)

Ref Expression
Hypotheses disjif.1 
|- F/_ x C
disjif.2 
|- ( x = Y -> B = C )
Assertion disji2f 
|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ x =/= Y ) -> ( B i^i C ) = (/) )

Proof

Step Hyp Ref Expression
1 disjif.1 
 |-  F/_ x C
2 disjif.2 
 |-  ( x = Y -> B = C )
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 equequ1 
 |-  ( y = x -> ( y = z <-> x = z ) )
6 csbeq1 
 |-  ( y = x -> [_ y / x ]_ B = [_ x / x ]_ B )
7 csbid 
 |-  [_ x / x ]_ B = B
8 6 7 eqtrdi 
 |-  ( y = x -> [_ y / x ]_ B = B )
9 8 ineq1d 
 |-  ( y = x -> ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = ( B i^i [_ z / x ]_ B ) )
10 9 eqeq1d 
 |-  ( y = x -> ( ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) <-> ( B i^i [_ z / x ]_ B ) = (/) ) )
11 5 10 orbi12d 
 |-  ( y = x -> ( ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) <-> ( x = z \/ ( B i^i [_ z / x ]_ B ) = (/) ) ) )
12 eqeq2 
 |-  ( z = Y -> ( x = z <-> x = Y ) )
13 nfcv 
 |-  F/_ x Y
14 13 1 2 csbhypf 
 |-  ( z = Y -> [_ z / x ]_ B = C )
15 14 ineq2d 
 |-  ( z = Y -> ( B i^i [_ z / x ]_ B ) = ( B i^i C ) )
16 15 eqeq1d 
 |-  ( z = Y -> ( ( B i^i [_ z / x ]_ B ) = (/) <-> ( B i^i C ) = (/) ) )
17 12 16 orbi12d 
 |-  ( z = Y -> ( ( x = z \/ ( B i^i [_ z / x ]_ B ) = (/) ) <-> ( x = Y \/ ( B i^i C ) = (/) ) ) )
18 11 17 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 \/ ( B i^i C ) = (/) ) ) )
19 4 18 syl5bi 
 |-  ( ( x e. A /\ Y e. A ) -> ( Disj_ x e. A B -> ( x = Y \/ ( B i^i C ) = (/) ) ) )
20 19 impcom 
 |-  ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) ) -> ( x = Y \/ ( B i^i C ) = (/) ) )
21 20 ord 
 |-  ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) ) -> ( -. x = Y -> ( B i^i C ) = (/) ) )
22 3 21 syl5bi 
 |-  ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) ) -> ( x =/= Y -> ( B i^i C ) = (/) ) )
23 22 3impia 
 |-  ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ x =/= Y ) -> ( B i^i C ) = (/) )