Metamath Proof Explorer

Theorem disjxp1

Description: The sets of a cartesian product are disjoint if the sets in the first argument are disjoint. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypothesis disjxp1.1 
|- ( ph -> Disj_ x e. A B )
Assertion disjxp1 
|- ( ph -> Disj_ x e. A ( B X. C ) )

Proof

Step Hyp Ref Expression
1 disjxp1.1 
 |-  ( ph -> Disj_ x e. A B )
2 animorrl 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y = z ) -> ( y = z \/ ( [_ y / x ]_ ( B X. C ) i^i [_ z / x ]_ ( B X. C ) ) = (/) ) )
3 csbxp 
 |-  [_ y / x ]_ ( B X. C ) = ( [_ y / x ]_ B X. [_ y / x ]_ C )
4 csbxp 
 |-  [_ z / x ]_ ( B X. C ) = ( [_ z / x ]_ B X. [_ z / x ]_ C )
5 3 4 ineq12i 
 |-  ( [_ y / x ]_ ( B X. C ) i^i [_ z / x ]_ ( B X. C ) ) = ( ( [_ y / x ]_ B X. [_ y / x ]_ C ) i^i ( [_ z / x ]_ B X. [_ z / x ]_ C ) )
6 simpll 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> ph )
7 simplrl 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> y e. A )
8 simplrr 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> z e. A )
9 6 7 8 jca31 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> ( ( ph /\ y e. A ) /\ z e. A ) )
10 simpr 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> y =/= z )
11 10 neneqd 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> -. y = z )
12 disjors 
 |-  ( Disj_ x e. A B <-> A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) )
13 1 12 sylib 
 |-  ( ph -> A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) )
14 13 r19.21bi 
 |-  ( ( ph /\ y e. A ) -> A. z e. A ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) )
15 14 r19.21bi 
 |-  ( ( ( ph /\ y e. A ) /\ z e. A ) -> ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) )
16 15 ord 
 |-  ( ( ( ph /\ y e. A ) /\ z e. A ) -> ( -. y = z -> ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) )
17 9 11 16 sylc 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) )
18 xpdisj1 
 |-  ( ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) -> ( ( [_ y / x ]_ B X. [_ y / x ]_ C ) i^i ( [_ z / x ]_ B X. [_ z / x ]_ C ) ) = (/) )
19 17 18 syl 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> ( ( [_ y / x ]_ B X. [_ y / x ]_ C ) i^i ( [_ z / x ]_ B X. [_ z / x ]_ C ) ) = (/) )
20 5 19 syl5eq 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> ( [_ y / x ]_ ( B X. C ) i^i [_ z / x ]_ ( B X. C ) ) = (/) )
21 20 olcd 
 |-  ( ( ( ph /\ ( y e. A /\ z e. A ) ) /\ y =/= z ) -> ( y = z \/ ( [_ y / x ]_ ( B X. C ) i^i [_ z / x ]_ ( B X. C ) ) = (/) ) )
22 2 21 pm2.61dane 
 |-  ( ( ph /\ ( y e. A /\ z e. A ) ) -> ( y = z \/ ( [_ y / x ]_ ( B X. C ) i^i [_ z / x ]_ ( B X. C ) ) = (/) ) )
23 22 ralrimivva 
 |-  ( ph -> A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ ( B X. C ) i^i [_ z / x ]_ ( B X. C ) ) = (/) ) )
24 disjors 
 |-  ( Disj_ x e. A ( B X. C ) <-> A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ ( B X. C ) i^i [_ z / x ]_ ( B X. C ) ) = (/) ) )
25 23 24 sylibr 
 |-  ( ph -> Disj_ x e. A ( B X. C ) )