Metamath Proof Explorer

Theorem boxcutc

Description: The relative complement of a box set restricted on one axis. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion boxcutc ⊢X∈A∧∀k∈AC⊆B→⨉k∈AB∖⨉k∈Aifk=XCB=⨉k∈Aifk=XB∖CB

Proof

Step Hyp Ref Expression
1 eldifi ⊢z∈⨉k∈AB∖⨉k∈Aifk=XCB→z∈⨉k∈AB
2 1 adantl ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∖⨉k∈Aifk=XCB→z∈⨉k∈AB
3 sseq1 ⊢B∖C=ifk=XB∖CB→B∖C⊆B↔ifk=XB∖CB⊆B
4 sseq1 ⊢B=ifk=XB∖CB→B⊆B↔ifk=XB∖CB⊆B
5 difss ⊢B∖C⊆B
6 ssid ⊢B⊆B
7 3 4 5 6 keephyp ⊢ifk=XB∖CB⊆B
8 7 rgenw ⊢∀k∈Aifk=XB∖CB⊆B
9 ss2ixp ⊢∀k∈Aifk=XB∖CB⊆B→⨉k∈Aifk=XB∖CB⊆⨉k∈AB
10 8 9 mp1i ⊢X∈A∧∀k∈AC⊆B→⨉k∈Aifk=XB∖CB⊆⨉k∈AB
11 10 sselda ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈Aifk=XB∖CB→z∈⨉k∈AB
12 vex ⊢z∈V
13 12 elixp ⊢z∈⨉k∈Aifk=XCB↔zFnA∧∀k∈Az⁡k∈ifk=XCB
14 ixpfn ⊢z∈⨉k∈AB→zFnA
15 14 adantl ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→zFnA
16 15 biantrurd ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→∀k∈Az⁡k∈ifk=XCB↔zFnA∧∀k∈Az⁡k∈ifk=XCB
17 13 16 bitr4id ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→z∈⨉k∈Aifk=XCB↔∀k∈Az⁡k∈ifk=XCB
18 17 notbid ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→¬z∈⨉k∈Aifk=XCB↔¬∀k∈Az⁡k∈ifk=XCB
19 rexnal ⊢∃k∈A¬z⁡k∈ifk=XCB↔¬∀k∈Az⁡k∈ifk=XCB
20 eleq2 ⊢⦋m/k⦌B∖⦋m/k⦌C=ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B→z⁡m∈⦋m/k⦌B∖⦋m/k⦌C↔z⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
21 eleq2 ⊢⦋m/k⦌B=ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B→z⁡m∈⦋m/k⦌B↔z⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
22 eleq2 ⊢⦋l/k⦌C=ifl=X⦋l/k⦌C⦋l/k⦌B→z⁡l∈⦋l/k⦌C↔z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
23 eleq2 ⊢⦋l/k⦌B=ifl=X⦋l/k⦌C⦋l/k⦌B→z⁡l∈⦋l/k⦌B↔z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
24 simpl ⊢X∈A∧∀k∈AC⊆B→X∈A
25 12 elixp ⊢z∈⨉k∈AB↔zFnA∧∀k∈Az⁡k∈B
26 25 simprbi ⊢z∈⨉k∈AB→∀k∈Az⁡k∈B
27 nfv ⊢Ⅎlz⁡k∈B
28 nfcsb1v ⊢Ⅎ_k⦋l/k⦌B
29 28 nfel2 ⊢Ⅎkz⁡l∈⦋l/k⦌B
30 fveq2 ⊢k=l→z⁡k=z⁡l
31 csbeq1a ⊢k=l→B=⦋l/k⦌B
32 30 31 eleq12d ⊢k=l→z⁡k∈B↔z⁡l∈⦋l/k⦌B
33 27 29 32 cbvralw ⊢∀k∈Az⁡k∈B↔∀l∈Az⁡l∈⦋l/k⦌B
34 26 33 sylib ⊢z∈⨉k∈AB→∀l∈Az⁡l∈⦋l/k⦌B
35 fveq2 ⊢l=X→z⁡l=z⁡X
36 csbeq1 ⊢l=X→⦋l/k⦌B=⦋X/k⦌B
37 35 36 eleq12d ⊢l=X→z⁡l∈⦋l/k⦌B↔z⁡X∈⦋X/k⦌B
38 37 rspcva ⊢X∈A∧∀l∈Az⁡l∈⦋l/k⦌B→z⁡X∈⦋X/k⦌B
39 24 34 38 syl2an ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→z⁡X∈⦋X/k⦌B
40 neldif ⊢z⁡X∈⦋X/k⦌B∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C→z⁡X∈⦋X/k⦌C
41 39 40 sylan ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C→z⁡X∈⦋X/k⦌C
42 41 adantr ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C∧l∈A→z⁡X∈⦋X/k⦌C
43 csbeq1 ⊢l=X→⦋l/k⦌C=⦋X/k⦌C
44 35 43 eleq12d ⊢l=X→z⁡l∈⦋l/k⦌C↔z⁡X∈⦋X/k⦌C
45 42 44 syl5ibrcom ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C∧l∈A→l=X→z⁡l∈⦋l/k⦌C
46 45 imp ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C∧l∈A∧l=X→z⁡l∈⦋l/k⦌C
47 34 ad2antlr ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C→∀l∈Az⁡l∈⦋l/k⦌B
48 47 r19.21bi ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C∧l∈A→z⁡l∈⦋l/k⦌B
49 48 adantr ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C∧l∈A∧¬l=X→z⁡l∈⦋l/k⦌B
50 22 23 46 49 ifbothda ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C∧l∈A→z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
51 50 ralrimiva ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C→∀l∈Az⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
52 dfral2 ⊢∀l∈Az⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B↔¬∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
53 51 52 sylib ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C→¬∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
54 53 ex ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→¬z⁡X∈⦋X/k⦌B∖⦋X/k⦌C→¬∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
55 54 con4d ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B→z⁡X∈⦋X/k⦌B∖⦋X/k⦌C
56 55 imp ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B→z⁡X∈⦋X/k⦌B∖⦋X/k⦌C
57 56 adantr ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B∧m∈A→z⁡X∈⦋X/k⦌B∖⦋X/k⦌C
58 fveq2 ⊢m=X→z⁡m=z⁡X
59 csbeq1 ⊢m=X→⦋m/k⦌B=⦋X/k⦌B
60 csbeq1 ⊢m=X→⦋m/k⦌C=⦋X/k⦌C
61 59 60 difeq12d ⊢m=X→⦋m/k⦌B∖⦋m/k⦌C=⦋X/k⦌B∖⦋X/k⦌C
62 58 61 eleq12d ⊢m=X→z⁡m∈⦋m/k⦌B∖⦋m/k⦌C↔z⁡X∈⦋X/k⦌B∖⦋X/k⦌C
63 57 62 syl5ibrcom ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B∧m∈A→m=X→z⁡m∈⦋m/k⦌B∖⦋m/k⦌C
64 63 imp ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B∧m∈A∧m=X→z⁡m∈⦋m/k⦌B∖⦋m/k⦌C
65 nfv ⊢Ⅎmz⁡k∈B
66 nfcsb1v ⊢Ⅎ_k⦋m/k⦌B
67 66 nfel2 ⊢Ⅎkz⁡m∈⦋m/k⦌B
68 fveq2 ⊢k=m→z⁡k=z⁡m
69 csbeq1a ⊢k=m→B=⦋m/k⦌B
70 68 69 eleq12d ⊢k=m→z⁡k∈B↔z⁡m∈⦋m/k⦌B
71 65 67 70 cbvralw ⊢∀k∈Az⁡k∈B↔∀m∈Az⁡m∈⦋m/k⦌B
72 26 71 sylib ⊢z∈⨉k∈AB→∀m∈Az⁡m∈⦋m/k⦌B
73 72 ad2antlr ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B→∀m∈Az⁡m∈⦋m/k⦌B
74 73 r19.21bi ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B∧m∈A→z⁡m∈⦋m/k⦌B
75 74 adantr ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B∧m∈A∧¬m=X→z⁡m∈⦋m/k⦌B
76 20 21 64 75 ifbothda ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B∧m∈A→z⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
77 76 ralrimiva ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B→∀m∈Az⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
78 simpll ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→X∈A
79 iftrue ⊢m=X→ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B=⦋m/k⦌B∖⦋m/k⦌C
80 79 61 eqtrd ⊢m=X→ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B=⦋X/k⦌B∖⦋X/k⦌C
81 58 80 eleq12d ⊢m=X→z⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B↔z⁡X∈⦋X/k⦌B∖⦋X/k⦌C
82 81 rspcva ⊢X∈A∧∀m∈Az⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B→z⁡X∈⦋X/k⦌B∖⦋X/k⦌C
83 78 82 sylan ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∀m∈Az⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B→z⁡X∈⦋X/k⦌B∖⦋X/k⦌C
84 83 eldifbd ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∀m∈Az⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B→¬z⁡X∈⦋X/k⦌C
85 iftrue ⊢l=X→ifl=X⦋l/k⦌C⦋l/k⦌B=⦋l/k⦌C
86 85 43 eqtrd ⊢l=X→ifl=X⦋l/k⦌C⦋l/k⦌B=⦋X/k⦌C
87 35 86 eleq12d ⊢l=X→z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B↔z⁡X∈⦋X/k⦌C
88 87 notbid ⊢l=X→¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B↔¬z⁡X∈⦋X/k⦌C
89 88 rspcev ⊢X∈A∧¬z⁡X∈⦋X/k⦌C→∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
90 78 84 89 syl2an2r ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB∧∀m∈Az⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B→∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
91 77 90 impbida ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B↔∀m∈Az⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
92 nfv ⊢Ⅎl¬z⁡k∈ifk=XCB
93 nfv ⊢Ⅎkl=X
94 nfcsb1v ⊢Ⅎ_k⦋l/k⦌C
95 93 94 28 nfif ⊢Ⅎ_kifl=X⦋l/k⦌C⦋l/k⦌B
96 95 nfel2 ⊢Ⅎkz⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
97 96 nfn ⊢Ⅎk¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
98 eqeq1 ⊢k=l→k=X↔l=X
99 csbeq1a ⊢k=l→C=⦋l/k⦌C
100 98 99 31 ifbieq12d ⊢k=l→ifk=XCB=ifl=X⦋l/k⦌C⦋l/k⦌B
101 30 100 eleq12d ⊢k=l→z⁡k∈ifk=XCB↔z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
102 101 notbid ⊢k=l→¬z⁡k∈ifk=XCB↔¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
103 92 97 102 cbvrexw ⊢∃k∈A¬z⁡k∈ifk=XCB↔∃l∈A¬z⁡l∈ifl=X⦋l/k⦌C⦋l/k⦌B
104 nfv ⊢Ⅎmz⁡k∈ifk=XB∖CB
105 nfv ⊢Ⅎkm=X
106 nfcsb1v ⊢Ⅎ_k⦋m/k⦌C
107 66 106 nfdif ⊢Ⅎ_k⦋m/k⦌B∖⦋m/k⦌C
108 105 107 66 nfif ⊢Ⅎ_kifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
109 108 nfel2 ⊢Ⅎkz⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
110 eqeq1 ⊢k=m→k=X↔m=X
111 csbeq1a ⊢k=m→C=⦋m/k⦌C
112 69 111 difeq12d ⊢k=m→B∖C=⦋m/k⦌B∖⦋m/k⦌C
113 110 112 69 ifbieq12d ⊢k=m→ifk=XB∖CB=ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
114 68 113 eleq12d ⊢k=m→z⁡k∈ifk=XB∖CB↔z⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
115 104 109 114 cbvralw ⊢∀k∈Az⁡k∈ifk=XB∖CB↔∀m∈Az⁡m∈ifm=X⦋m/k⦌B∖⦋m/k⦌C⦋m/k⦌B
116 91 103 115 3bitr4g ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→∃k∈A¬z⁡k∈ifk=XCB↔∀k∈Az⁡k∈ifk=XB∖CB
117 19 116 bitr3id ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→¬∀k∈Az⁡k∈ifk=XCB↔∀k∈Az⁡k∈ifk=XB∖CB
118 18 117 bitrd ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→¬z∈⨉k∈Aifk=XCB↔∀k∈Az⁡k∈ifk=XB∖CB
119 ibar ⊢z∈⨉k∈AB→¬z∈⨉k∈Aifk=XCB↔z∈⨉k∈AB∧¬z∈⨉k∈Aifk=XCB
120 119 adantl ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→¬z∈⨉k∈Aifk=XCB↔z∈⨉k∈AB∧¬z∈⨉k∈Aifk=XCB
121 15 biantrurd ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→∀k∈Az⁡k∈ifk=XB∖CB↔zFnA∧∀k∈Az⁡k∈ifk=XB∖CB
122 118 120 121 3bitr3d ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→z∈⨉k∈AB∧¬z∈⨉k∈Aifk=XCB↔zFnA∧∀k∈Az⁡k∈ifk=XB∖CB
123 eldif ⊢z∈⨉k∈AB∖⨉k∈Aifk=XCB↔z∈⨉k∈AB∧¬z∈⨉k∈Aifk=XCB
124 12 elixp ⊢z∈⨉k∈Aifk=XB∖CB↔zFnA∧∀k∈Az⁡k∈ifk=XB∖CB
125 122 123 124 3bitr4g ⊢X∈A∧∀k∈AC⊆B∧z∈⨉k∈AB→z∈⨉k∈AB∖⨉k∈Aifk=XCB↔z∈⨉k∈Aifk=XB∖CB
126 2 11 125 eqrdav ⊢X∈A∧∀k∈AC⊆B→⨉k∈AB∖⨉k∈Aifk=XCB=⨉k∈Aifk=XB∖CB