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

Metamath Proof Explorer

Theorem disjif2

Description: Property of a disjoint collection: if B ( x ) and B ( Y ) = D have a common element Z , then x = Y . (Contributed by Thierry Arnoux, 6-Apr-2017)

Ref Expression
Hypotheses disjif2.1 
|- F/_ x A
disjif2.2 
|- F/_ x C
disjif2.3 
|- ( x = Y -> B = C )
Assertion disjif2 
|- ( ( Disj_ x e. A B /\ ( x e. A /\ Y e. A ) /\ ( Z e. B /\ Z e. C ) ) -> x = Y )

Proof

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