Metamath Proof Explorer

Theorem disjxpin

Description: Derive a disjunction over a Cartesian product from the disjunctions over its first and second elements. (Contributed by Thierry Arnoux, 9-Mar-2018)

Ref Expression
Hypotheses disjxpin.1 
|- ( x = ( 1st ` p ) -> C = E )
disjxpin.2 
|- ( y = ( 2nd ` p ) -> D = F )
disjxpin.3 
|- ( ph -> Disj_ x e. A C )
disjxpin.4 
|- ( ph -> Disj_ y e. B D )
Assertion disjxpin 
|- ( ph -> Disj_ p e. ( A X. B ) ( E i^i F ) )

Proof

Step Hyp Ref Expression
1 disjxpin.1 
 |-  ( x = ( 1st ` p ) -> C = E )
2 disjxpin.2 
 |-  ( y = ( 2nd ` p ) -> D = F )
3 disjxpin.3 
 |-  ( ph -> Disj_ x e. A C )
4 disjxpin.4 
 |-  ( ph -> Disj_ y e. B D )
5 xp1st 
 |-  ( q e. ( A X. B ) -> ( 1st ` q ) e. A )
6 5 ad2antrl 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( 1st ` q ) e. A )
7 xp1st 
 |-  ( r e. ( A X. B ) -> ( 1st ` r ) e. A )
8 7 ad2antll 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( 1st ` r ) e. A )
9 simpl 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ph )
10 disjors 
 |-  ( Disj_ x e. A C <-> A. a e. A A. c e. A ( a = c \/ ( [_ a / x ]_ C i^i [_ c / x ]_ C ) = (/) ) )
11 3 10 sylib 
 |-  ( ph -> A. a e. A A. c e. A ( a = c \/ ( [_ a / x ]_ C i^i [_ c / x ]_ C ) = (/) ) )
12 eqeq1 
 |-  ( a = ( 1st ` q ) -> ( a = c <-> ( 1st ` q ) = c ) )
13 csbeq1 
 |-  ( a = ( 1st ` q ) -> [_ a / x ]_ C = [_ ( 1st ` q ) / x ]_ C )
14 13 ineq1d 
 |-  ( a = ( 1st ` q ) -> ( [_ a / x ]_ C i^i [_ c / x ]_ C ) = ( [_ ( 1st ` q ) / x ]_ C i^i [_ c / x ]_ C ) )
15 14 eqeq1d 
 |-  ( a = ( 1st ` q ) -> ( ( [_ a / x ]_ C i^i [_ c / x ]_ C ) = (/) <-> ( [_ ( 1st ` q ) / x ]_ C i^i [_ c / x ]_ C ) = (/) ) )
16 12 15 orbi12d 
 |-  ( a = ( 1st ` q ) -> ( ( a = c \/ ( [_ a / x ]_ C i^i [_ c / x ]_ C ) = (/) ) <-> ( ( 1st ` q ) = c \/ ( [_ ( 1st ` q ) / x ]_ C i^i [_ c / x ]_ C ) = (/) ) ) )
17 eqeq2 
 |-  ( c = ( 1st ` r ) -> ( ( 1st ` q ) = c <-> ( 1st ` q ) = ( 1st ` r ) ) )
18 csbeq1 
 |-  ( c = ( 1st ` r ) -> [_ c / x ]_ C = [_ ( 1st ` r ) / x ]_ C )
19 18 ineq2d 
 |-  ( c = ( 1st ` r ) -> ( [_ ( 1st ` q ) / x ]_ C i^i [_ c / x ]_ C ) = ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) )
20 19 eqeq1d 
 |-  ( c = ( 1st ` r ) -> ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ c / x ]_ C ) = (/) <-> ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) ) )
21 17 20 orbi12d 
 |-  ( c = ( 1st ` r ) -> ( ( ( 1st ` q ) = c \/ ( [_ ( 1st ` q ) / x ]_ C i^i [_ c / x ]_ C ) = (/) ) <-> ( ( 1st ` q ) = ( 1st ` r ) \/ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) ) ) )
22 16 21 rspc2v 
 |-  ( ( ( 1st ` q ) e. A /\ ( 1st ` r ) e. A ) -> ( A. a e. A A. c e. A ( a = c \/ ( [_ a / x ]_ C i^i [_ c / x ]_ C ) = (/) ) -> ( ( 1st ` q ) = ( 1st ` r ) \/ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) ) ) )
23 11 22 syl5 
 |-  ( ( ( 1st ` q ) e. A /\ ( 1st ` r ) e. A ) -> ( ph -> ( ( 1st ` q ) = ( 1st ` r ) \/ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) ) ) )
24 23 imp 
 |-  ( ( ( ( 1st ` q ) e. A /\ ( 1st ` r ) e. A ) /\ ph ) -> ( ( 1st ` q ) = ( 1st ` r ) \/ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) ) )
25 6 8 9 24 syl21anc 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( 1st ` q ) = ( 1st ` r ) \/ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) ) )
26 xp2nd 
 |-  ( q e. ( A X. B ) -> ( 2nd ` q ) e. B )
27 26 ad2antrl 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( 2nd ` q ) e. B )
28 xp2nd 
 |-  ( r e. ( A X. B ) -> ( 2nd ` r ) e. B )
29 28 ad2antll 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( 2nd ` r ) e. B )
30 disjors 
 |-  ( Disj_ y e. B D <-> A. b e. B A. d e. B ( b = d \/ ( [_ b / y ]_ D i^i [_ d / y ]_ D ) = (/) ) )
31 4 30 sylib 
 |-  ( ph -> A. b e. B A. d e. B ( b = d \/ ( [_ b / y ]_ D i^i [_ d / y ]_ D ) = (/) ) )
32 eqeq1 
 |-  ( b = ( 2nd ` q ) -> ( b = d <-> ( 2nd ` q ) = d ) )
33 csbeq1 
 |-  ( b = ( 2nd ` q ) -> [_ b / y ]_ D = [_ ( 2nd ` q ) / y ]_ D )
34 33 ineq1d 
 |-  ( b = ( 2nd ` q ) -> ( [_ b / y ]_ D i^i [_ d / y ]_ D ) = ( [_ ( 2nd ` q ) / y ]_ D i^i [_ d / y ]_ D ) )
35 34 eqeq1d 
 |-  ( b = ( 2nd ` q ) -> ( ( [_ b / y ]_ D i^i [_ d / y ]_ D ) = (/) <-> ( [_ ( 2nd ` q ) / y ]_ D i^i [_ d / y ]_ D ) = (/) ) )
36 32 35 orbi12d 
 |-  ( b = ( 2nd ` q ) -> ( ( b = d \/ ( [_ b / y ]_ D i^i [_ d / y ]_ D ) = (/) ) <-> ( ( 2nd ` q ) = d \/ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ d / y ]_ D ) = (/) ) ) )
37 eqeq2 
 |-  ( d = ( 2nd ` r ) -> ( ( 2nd ` q ) = d <-> ( 2nd ` q ) = ( 2nd ` r ) ) )
38 csbeq1 
 |-  ( d = ( 2nd ` r ) -> [_ d / y ]_ D = [_ ( 2nd ` r ) / y ]_ D )
39 38 ineq2d 
 |-  ( d = ( 2nd ` r ) -> ( [_ ( 2nd ` q ) / y ]_ D i^i [_ d / y ]_ D ) = ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) )
40 39 eqeq1d 
 |-  ( d = ( 2nd ` r ) -> ( ( [_ ( 2nd ` q ) / y ]_ D i^i [_ d / y ]_ D ) = (/) <-> ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) )
41 37 40 orbi12d 
 |-  ( d = ( 2nd ` r ) -> ( ( ( 2nd ` q ) = d \/ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ d / y ]_ D ) = (/) ) <-> ( ( 2nd ` q ) = ( 2nd ` r ) \/ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) )
42 36 41 rspc2v 
 |-  ( ( ( 2nd ` q ) e. B /\ ( 2nd ` r ) e. B ) -> ( A. b e. B A. d e. B ( b = d \/ ( [_ b / y ]_ D i^i [_ d / y ]_ D ) = (/) ) -> ( ( 2nd ` q ) = ( 2nd ` r ) \/ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) )
43 31 42 syl5 
 |-  ( ( ( 2nd ` q ) e. B /\ ( 2nd ` r ) e. B ) -> ( ph -> ( ( 2nd ` q ) = ( 2nd ` r ) \/ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) )
44 43 imp 
 |-  ( ( ( ( 2nd ` q ) e. B /\ ( 2nd ` r ) e. B ) /\ ph ) -> ( ( 2nd ` q ) = ( 2nd ` r ) \/ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) )
45 27 29 9 44 syl21anc 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( 2nd ` q ) = ( 2nd ` r ) \/ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) )
46 25 45 jca 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( 1st ` q ) = ( 1st ` r ) \/ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) ) /\ ( ( 2nd ` q ) = ( 2nd ` r ) \/ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) )
47 anddi 
 |-  ( ( ( ( 1st ` q ) = ( 1st ` r ) \/ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) ) /\ ( ( 2nd ` q ) = ( 2nd ` r ) \/ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) <-> ( ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( 1st ` q ) = ( 1st ` r ) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) \/ ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) ) )
48 46 47 sylib 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( 1st ` q ) = ( 1st ` r ) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) \/ ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) ) )
49 orass 
 |-  ( ( ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( 1st ` q ) = ( 1st ` r ) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) \/ ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) ) <-> ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) \/ ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) ) ) )
50 48 49 sylib 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) \/ ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) ) ) )
51 xpopth 
 |-  ( ( q e. ( A X. B ) /\ r e. ( A X. B ) ) -> ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( 2nd ` q ) = ( 2nd ` r ) ) <-> q = r ) )
52 51 adantl 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( 2nd ` q ) = ( 2nd ` r ) ) <-> q = r ) )
53 52 biimpd 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( 2nd ` q ) = ( 2nd ` r ) ) -> q = r ) )
54 inss2 
 |-  ( ( [_ q / p ]_ E i^i [_ r / p ]_ E ) i^i ( [_ q / p ]_ F i^i [_ r / p ]_ F ) ) C_ ( [_ q / p ]_ F i^i [_ r / p ]_ F )
55 csbin 
 |-  [_ q / p ]_ ( E i^i F ) = ( [_ q / p ]_ E i^i [_ q / p ]_ F )
56 csbin 
 |-  [_ r / p ]_ ( E i^i F ) = ( [_ r / p ]_ E i^i [_ r / p ]_ F )
57 55 56 ineq12i 
 |-  ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = ( ( [_ q / p ]_ E i^i [_ q / p ]_ F ) i^i ( [_ r / p ]_ E i^i [_ r / p ]_ F ) )
58 in4 
 |-  ( ( [_ q / p ]_ E i^i [_ q / p ]_ F ) i^i ( [_ r / p ]_ E i^i [_ r / p ]_ F ) ) = ( ( [_ q / p ]_ E i^i [_ r / p ]_ E ) i^i ( [_ q / p ]_ F i^i [_ r / p ]_ F ) )
59 57 58 eqtri 
 |-  ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = ( ( [_ q / p ]_ E i^i [_ r / p ]_ E ) i^i ( [_ q / p ]_ F i^i [_ r / p ]_ F ) )
60 vex 
 |-  q e. _V
61 csbnestgw 
 |-  ( q e. _V -> [_ q / p ]_ [_ ( 2nd ` p ) / y ]_ D = [_ [_ q / p ]_ ( 2nd ` p ) / y ]_ D )
62 60 61 ax-mp 
 |-  [_ q / p ]_ [_ ( 2nd ` p ) / y ]_ D = [_ [_ q / p ]_ ( 2nd ` p ) / y ]_ D
63 fvex 
 |-  ( 2nd ` p ) e. _V
64 63 2 csbie 
 |-  [_ ( 2nd ` p ) / y ]_ D = F
65 64 csbeq2i 
 |-  [_ q / p ]_ [_ ( 2nd ` p ) / y ]_ D = [_ q / p ]_ F
66 csbfv 
 |-  [_ q / p ]_ ( 2nd ` p ) = ( 2nd ` q )
67 csbeq1 
 |-  ( [_ q / p ]_ ( 2nd ` p ) = ( 2nd ` q ) -> [_ [_ q / p ]_ ( 2nd ` p ) / y ]_ D = [_ ( 2nd ` q ) / y ]_ D )
68 66 67 ax-mp 
 |-  [_ [_ q / p ]_ ( 2nd ` p ) / y ]_ D = [_ ( 2nd ` q ) / y ]_ D
69 62 65 68 3eqtr3ri 
 |-  [_ ( 2nd ` q ) / y ]_ D = [_ q / p ]_ F
70 vex 
 |-  r e. _V
71 csbnestgw 
 |-  ( r e. _V -> [_ r / p ]_ [_ ( 2nd ` p ) / y ]_ D = [_ [_ r / p ]_ ( 2nd ` p ) / y ]_ D )
72 70 71 ax-mp 
 |-  [_ r / p ]_ [_ ( 2nd ` p ) / y ]_ D = [_ [_ r / p ]_ ( 2nd ` p ) / y ]_ D
73 64 csbeq2i 
 |-  [_ r / p ]_ [_ ( 2nd ` p ) / y ]_ D = [_ r / p ]_ F
74 csbfv 
 |-  [_ r / p ]_ ( 2nd ` p ) = ( 2nd ` r )
75 csbeq1 
 |-  ( [_ r / p ]_ ( 2nd ` p ) = ( 2nd ` r ) -> [_ [_ r / p ]_ ( 2nd ` p ) / y ]_ D = [_ ( 2nd ` r ) / y ]_ D )
76 74 75 ax-mp 
 |-  [_ [_ r / p ]_ ( 2nd ` p ) / y ]_ D = [_ ( 2nd ` r ) / y ]_ D
77 72 73 76 3eqtr3ri 
 |-  [_ ( 2nd ` r ) / y ]_ D = [_ r / p ]_ F
78 69 77 ineq12i 
 |-  ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = ( [_ q / p ]_ F i^i [_ r / p ]_ F )
79 54 59 78 3sstr4i 
 |-  ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) C_ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D )
80 sseq0 
 |-  ( ( ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) C_ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) )
81 79 80 mpan 
 |-  ( ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) )
82 81 a1i 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
83 82 adantld 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
84 inss1 
 |-  ( ( [_ q / p ]_ E i^i [_ r / p ]_ E ) i^i ( [_ q / p ]_ F i^i [_ r / p ]_ F ) ) C_ ( [_ q / p ]_ E i^i [_ r / p ]_ E )
85 csbnestgw 
 |-  ( q e. _V -> [_ q / p ]_ [_ ( 1st ` p ) / x ]_ C = [_ [_ q / p ]_ ( 1st ` p ) / x ]_ C )
86 60 85 ax-mp 
 |-  [_ q / p ]_ [_ ( 1st ` p ) / x ]_ C = [_ [_ q / p ]_ ( 1st ` p ) / x ]_ C
87 fvex 
 |-  ( 1st ` p ) e. _V
88 87 1 csbie 
 |-  [_ ( 1st ` p ) / x ]_ C = E
89 88 csbeq2i 
 |-  [_ q / p ]_ [_ ( 1st ` p ) / x ]_ C = [_ q / p ]_ E
90 csbfv 
 |-  [_ q / p ]_ ( 1st ` p ) = ( 1st ` q )
91 csbeq1 
 |-  ( [_ q / p ]_ ( 1st ` p ) = ( 1st ` q ) -> [_ [_ q / p ]_ ( 1st ` p ) / x ]_ C = [_ ( 1st ` q ) / x ]_ C )
92 90 91 ax-mp 
 |-  [_ [_ q / p ]_ ( 1st ` p ) / x ]_ C = [_ ( 1st ` q ) / x ]_ C
93 86 89 92 3eqtr3ri 
 |-  [_ ( 1st ` q ) / x ]_ C = [_ q / p ]_ E
94 csbnestgw 
 |-  ( r e. _V -> [_ r / p ]_ [_ ( 1st ` p ) / x ]_ C = [_ [_ r / p ]_ ( 1st ` p ) / x ]_ C )
95 70 94 ax-mp 
 |-  [_ r / p ]_ [_ ( 1st ` p ) / x ]_ C = [_ [_ r / p ]_ ( 1st ` p ) / x ]_ C
96 88 csbeq2i 
 |-  [_ r / p ]_ [_ ( 1st ` p ) / x ]_ C = [_ r / p ]_ E
97 csbfv 
 |-  [_ r / p ]_ ( 1st ` p ) = ( 1st ` r )
98 csbeq1 
 |-  ( [_ r / p ]_ ( 1st ` p ) = ( 1st ` r ) -> [_ [_ r / p ]_ ( 1st ` p ) / x ]_ C = [_ ( 1st ` r ) / x ]_ C )
99 97 98 ax-mp 
 |-  [_ [_ r / p ]_ ( 1st ` p ) / x ]_ C = [_ ( 1st ` r ) / x ]_ C
100 95 96 99 3eqtr3ri 
 |-  [_ ( 1st ` r ) / x ]_ C = [_ r / p ]_ E
101 93 100 ineq12i 
 |-  ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = ( [_ q / p ]_ E i^i [_ r / p ]_ E )
102 84 59 101 3sstr4i 
 |-  ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) C_ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C )
103 sseq0 
 |-  ( ( ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) C_ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) /\ ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) ) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) )
104 102 103 mpan 
 |-  ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) )
105 104 a1i 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
106 105 adantrd 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( 2nd ` q ) = ( 2nd ` r ) ) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
107 82 adantld 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
108 106 107 jaod 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
109 83 108 jaod 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) \/ ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) ) -> ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
110 53 109 orim12d 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( ( 1st ` q ) = ( 1st ` r ) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) \/ ( ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( 2nd ` q ) = ( 2nd ` r ) ) \/ ( ( [_ ( 1st ` q ) / x ]_ C i^i [_ ( 1st ` r ) / x ]_ C ) = (/) /\ ( [_ ( 2nd ` q ) / y ]_ D i^i [_ ( 2nd ` r ) / y ]_ D ) = (/) ) ) ) ) -> ( q = r \/ ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) ) )
111 50 110 mpd 
 |-  ( ( ph /\ ( q e. ( A X. B ) /\ r e. ( A X. B ) ) ) -> ( q = r \/ ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
112 111 ralrimivva 
 |-  ( ph -> A. q e. ( A X. B ) A. r e. ( A X. B ) ( q = r \/ ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
113 disjors 
 |-  ( Disj_ p e. ( A X. B ) ( E i^i F ) <-> A. q e. ( A X. B ) A. r e. ( A X. B ) ( q = r \/ ( [_ q / p ]_ ( E i^i F ) i^i [_ r / p ]_ ( E i^i F ) ) = (/) ) )
114 112 113 sylibr 
 |-  ( ph -> Disj_ p e. ( A X. B ) ( E i^i F ) )