Metamath Proof Explorer

Theorem disjprg

Description: A pair collection is disjoint iff the two sets in the family have empty intersection. (Contributed by Mario Carneiro, 14-Nov-2016)

Ref Expression
Hypotheses disjprg.1 
|- ( x = A -> C = D )
disjprg.2 
|- ( x = B -> C = E )
Assertion disjprg 
|- ( ( A e. V /\ B e. V /\ A =/= B ) -> ( Disj_ x e. { A , B } C <-> ( D i^i E ) = (/) ) )

Proof

Step Hyp Ref Expression
1 disjprg.1 
 |-  ( x = A -> C = D )
2 disjprg.2 
 |-  ( x = B -> C = E )
3 eqeq1 
 |-  ( y = A -> ( y = z <-> A = z ) )
4 nfcv 
 |-  F/_ x A
5 nfcv 
 |-  F/_ x D
6 4 5 1 csbhypf 
 |-  ( y = A -> [_ y / x ]_ C = D )
7 6 ineq1d 
 |-  ( y = A -> ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = ( D i^i [_ z / x ]_ C ) )
8 7 eqeq1d 
 |-  ( y = A -> ( ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) <-> ( D i^i [_ z / x ]_ C ) = (/) ) )
9 3 8 orbi12d 
 |-  ( y = A -> ( ( y = z \/ ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) ) <-> ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) ) )
10 9 ralbidv 
 |-  ( y = A -> ( A. z e. { A , B } ( y = z \/ ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) ) <-> A. z e. { A , B } ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) ) )
11 eqeq1 
 |-  ( y = B -> ( y = z <-> B = z ) )
12 nfcv 
 |-  F/_ x B
13 nfcv 
 |-  F/_ x E
14 12 13 2 csbhypf 
 |-  ( y = B -> [_ y / x ]_ C = E )
15 14 ineq1d 
 |-  ( y = B -> ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = ( E i^i [_ z / x ]_ C ) )
16 15 eqeq1d 
 |-  ( y = B -> ( ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) <-> ( E i^i [_ z / x ]_ C ) = (/) ) )
17 11 16 orbi12d 
 |-  ( y = B -> ( ( y = z \/ ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) ) <-> ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) ) )
18 17 ralbidv 
 |-  ( y = B -> ( A. z e. { A , B } ( y = z \/ ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) ) <-> A. z e. { A , B } ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) ) )
19 10 18 ralprg 
 |-  ( ( A e. V /\ B e. V ) -> ( A. y e. { A , B } A. z e. { A , B } ( y = z \/ ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) ) <-> ( A. z e. { A , B } ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) /\ A. z e. { A , B } ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) ) ) )
20 19 3adant3 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( A. y e. { A , B } A. z e. { A , B } ( y = z \/ ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) ) <-> ( A. z e. { A , B } ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) /\ A. z e. { A , B } ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) ) ) )
21 id 
 |-  ( z = A -> z = A )
22 21 eqcomd 
 |-  ( z = A -> A = z )
23 22 orcd 
 |-  ( z = A -> ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) )
24 trud 
 |-  ( z = A -> T. )
25 23 24 2thd 
 |-  ( z = A -> ( ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) <-> T. ) )
26 eqeq2 
 |-  ( z = B -> ( A = z <-> A = B ) )
27 12 13 2 csbhypf 
 |-  ( z = B -> [_ z / x ]_ C = E )
28 27 ineq2d 
 |-  ( z = B -> ( D i^i [_ z / x ]_ C ) = ( D i^i E ) )
29 28 eqeq1d 
 |-  ( z = B -> ( ( D i^i [_ z / x ]_ C ) = (/) <-> ( D i^i E ) = (/) ) )
30 26 29 orbi12d 
 |-  ( z = B -> ( ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) <-> ( A = B \/ ( D i^i E ) = (/) ) ) )
31 25 30 ralprg 
 |-  ( ( A e. V /\ B e. V ) -> ( A. z e. { A , B } ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) <-> ( T. /\ ( A = B \/ ( D i^i E ) = (/) ) ) ) )
32 31 3adant3 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( A. z e. { A , B } ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) <-> ( T. /\ ( A = B \/ ( D i^i E ) = (/) ) ) ) )
33 simp3 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> A =/= B )
34 33 neneqd 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> -. A = B )
35 biorf 
 |-  ( -. A = B -> ( ( D i^i E ) = (/) <-> ( A = B \/ ( D i^i E ) = (/) ) ) )
36 34 35 syl 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( ( D i^i E ) = (/) <-> ( A = B \/ ( D i^i E ) = (/) ) ) )
37 tru 
 |-  T.
38 37 biantrur 
 |-  ( ( A = B \/ ( D i^i E ) = (/) ) <-> ( T. /\ ( A = B \/ ( D i^i E ) = (/) ) ) )
39 36 38 bitrdi 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( ( D i^i E ) = (/) <-> ( T. /\ ( A = B \/ ( D i^i E ) = (/) ) ) ) )
40 32 39 bitr4d 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( A. z e. { A , B } ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) <-> ( D i^i E ) = (/) ) )
41 eqeq2 
 |-  ( z = A -> ( B = z <-> B = A ) )
42 eqcom 
 |-  ( B = A <-> A = B )
43 41 42 bitrdi 
 |-  ( z = A -> ( B = z <-> A = B ) )
44 4 5 1 csbhypf 
 |-  ( z = A -> [_ z / x ]_ C = D )
45 44 ineq2d 
 |-  ( z = A -> ( E i^i [_ z / x ]_ C ) = ( E i^i D ) )
46 incom 
 |-  ( E i^i D ) = ( D i^i E )
47 45 46 eqtrdi 
 |-  ( z = A -> ( E i^i [_ z / x ]_ C ) = ( D i^i E ) )
48 47 eqeq1d 
 |-  ( z = A -> ( ( E i^i [_ z / x ]_ C ) = (/) <-> ( D i^i E ) = (/) ) )
49 43 48 orbi12d 
 |-  ( z = A -> ( ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) <-> ( A = B \/ ( D i^i E ) = (/) ) ) )
50 id 
 |-  ( z = B -> z = B )
51 50 eqcomd 
 |-  ( z = B -> B = z )
52 51 orcd 
 |-  ( z = B -> ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) )
53 trud 
 |-  ( z = B -> T. )
54 52 53 2thd 
 |-  ( z = B -> ( ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) <-> T. ) )
55 49 54 ralprg 
 |-  ( ( A e. V /\ B e. V ) -> ( A. z e. { A , B } ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) <-> ( ( A = B \/ ( D i^i E ) = (/) ) /\ T. ) ) )
56 55 3adant3 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( A. z e. { A , B } ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) <-> ( ( A = B \/ ( D i^i E ) = (/) ) /\ T. ) ) )
57 37 biantru 
 |-  ( ( A = B \/ ( D i^i E ) = (/) ) <-> ( ( A = B \/ ( D i^i E ) = (/) ) /\ T. ) )
58 36 57 bitrdi 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( ( D i^i E ) = (/) <-> ( ( A = B \/ ( D i^i E ) = (/) ) /\ T. ) ) )
59 56 58 bitr4d 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( A. z e. { A , B } ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) <-> ( D i^i E ) = (/) ) )
60 40 59 anbi12d 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( ( A. z e. { A , B } ( A = z \/ ( D i^i [_ z / x ]_ C ) = (/) ) /\ A. z e. { A , B } ( B = z \/ ( E i^i [_ z / x ]_ C ) = (/) ) ) <-> ( ( D i^i E ) = (/) /\ ( D i^i E ) = (/) ) ) )
61 20 60 bitrd 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( A. y e. { A , B } A. z e. { A , B } ( y = z \/ ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) ) <-> ( ( D i^i E ) = (/) /\ ( D i^i E ) = (/) ) ) )
62 disjors 
 |-  ( Disj_ x e. { A , B } C <-> A. y e. { A , B } A. z e. { A , B } ( y = z \/ ( [_ y / x ]_ C i^i [_ z / x ]_ C ) = (/) ) )
63 pm4.24 
 |-  ( ( D i^i E ) = (/) <-> ( ( D i^i E ) = (/) /\ ( D i^i E ) = (/) ) )
64 61 62 63 3bitr4g 
 |-  ( ( A e. V /\ B e. V /\ A =/= B ) -> ( Disj_ x e. { A , B } C <-> ( D i^i E ) = (/) ) )