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 ) )