# 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 ${⊢}\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\to \underset{{k}\in {A}}{⨉}{B}\setminus \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)=\underset{{k}\in {A}}{⨉}if\left({k}={X},{B}\setminus {C},{B}\right)$

### Proof

Step Hyp Ref Expression
1 eldifi ${⊢}{z}\in \left(\underset{{k}\in {A}}{⨉}{B}\setminus \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)\right)\to {z}\in \underset{{k}\in {A}}{⨉}{B}$
2 1 adantl ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \left(\underset{{k}\in {A}}{⨉}{B}\setminus \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)\right)\right)\to {z}\in \underset{{k}\in {A}}{⨉}{B}$
3 sseq1 ${⊢}{B}\setminus {C}=if\left({k}={X},{B}\setminus {C},{B}\right)\to \left({B}\setminus {C}\subseteq {B}↔if\left({k}={X},{B}\setminus {C},{B}\right)\subseteq {B}\right)$
4 sseq1 ${⊢}{B}=if\left({k}={X},{B}\setminus {C},{B}\right)\to \left({B}\subseteq {B}↔if\left({k}={X},{B}\setminus {C},{B}\right)\subseteq {B}\right)$
5 difss ${⊢}{B}\setminus {C}\subseteq {B}$
6 ssid ${⊢}{B}\subseteq {B}$
7 3 4 5 6 keephyp ${⊢}if\left({k}={X},{B}\setminus {C},{B}\right)\subseteq {B}$
8 7 rgenw ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}if\left({k}={X},{B}\setminus {C},{B}\right)\subseteq {B}$
9 ss2ixp ${⊢}\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}if\left({k}={X},{B}\setminus {C},{B}\right)\subseteq {B}\to \underset{{k}\in {A}}{⨉}if\left({k}={X},{B}\setminus {C},{B}\right)\subseteq \underset{{k}\in {A}}{⨉}{B}$
10 8 9 mp1i ${⊢}\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\to \underset{{k}\in {A}}{⨉}if\left({k}={X},{B}\setminus {C},{B}\right)\subseteq \underset{{k}\in {A}}{⨉}{B}$
11 10 sselda ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{B}\setminus {C},{B}\right)\right)\to {z}\in \underset{{k}\in {A}}{⨉}{B}$
12 ixpfn ${⊢}{z}\in \underset{{k}\in {A}}{⨉}{B}\to {z}Fn{A}$
13 12 adantl ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to {z}Fn{A}$
14 13 biantrurd ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)↔\left({z}Fn{A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)\right)\right)$
15 vex ${⊢}{z}\in \mathrm{V}$
16 15 elixp ${⊢}{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)↔\left({z}Fn{A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)\right)$
17 14 16 syl6rbbr ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left({z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)↔\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)\right)$
18 17 notbid ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left(¬{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)↔¬\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)\right)$
19 rexnal ${⊢}\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}¬{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)↔¬\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)$
20 eleq2
21 eleq2
22 eleq2
23 eleq2
24 simpl ${⊢}\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\to {X}\in {A}$
25 15 elixp ${⊢}{z}\in \underset{{k}\in {A}}{⨉}{B}↔\left({z}Fn{A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in {B}\right)$
26 25 simprbi ${⊢}{z}\in \underset{{k}\in {A}}{⨉}{B}\to \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in {B}$
27 nfv ${⊢}Ⅎ{l}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in {B}$
28 nfcsb1v
29 28 nfel2
30 fveq2 ${⊢}{k}={l}\to {z}\left({k}\right)={z}\left({l}\right)$
31 csbeq1a
32 30 31 eleq12d
33 27 29 32 cbvralw
34 26 33 sylib
35 fveq2 ${⊢}{l}={X}\to {z}\left({l}\right)={z}\left({X}\right)$
36 csbeq1
37 35 36 eleq12d
38 37 rspcva
39 24 34 38 syl2an
40 neldif
41 39 40 sylan
43 csbeq1
44 35 43 eleq12d
45 42 44 syl5ibrcom
46 45 imp
48 47 r19.21bi
50 22 23 46 49 ifbothda
51 50 ralrimiva
52 dfral2
53 51 52 sylib
54 53 ex
55 54 con4d
56 55 imp
58 fveq2 ${⊢}{m}={X}\to {z}\left({m}\right)={z}\left({X}\right)$
59 csbeq1
60 csbeq1
61 59 60 difeq12d
62 58 61 eleq12d
63 57 62 syl5ibrcom
64 63 imp
65 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in {B}$
66 nfcsb1v
67 66 nfel2
68 fveq2 ${⊢}{k}={m}\to {z}\left({k}\right)={z}\left({m}\right)$
69 csbeq1a
70 68 69 eleq12d
71 65 67 70 cbvralw
72 26 71 sylib
74 73 r19.21bi
76 20 21 64 75 ifbothda
77 76 ralrimiva
78 simpll ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to {X}\in {A}$
79 iftrue
80 79 61 eqtrd
81 58 80 eleq12d
82 81 rspcva
83 78 82 sylan
84 83 eldifbd
85 iftrue
86 85 43 eqtrd
87 35 86 eleq12d
88 87 notbid
89 88 rspcev
90 78 84 89 syl2an2r
91 77 90 impbida
92 nfv ${⊢}Ⅎ{l}\phantom{\rule{.4em}{0ex}}¬{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)$
93 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{l}={X}$
94 nfcsb1v
95 93 94 28 nfif
96 95 nfel2
97 96 nfn
98 eqeq1 ${⊢}{k}={l}\to \left({k}={X}↔{l}={X}\right)$
99 csbeq1a
100 98 99 31 ifbieq12d
101 30 100 eleq12d
102 101 notbid
103 92 97 102 cbvrexw
104 nfv ${⊢}Ⅎ{m}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{B}\setminus {C},{B}\right)$
105 nfv ${⊢}Ⅎ{k}\phantom{\rule{.4em}{0ex}}{m}={X}$
106 nfcsb1v
107 66 106 nfdif
108 105 107 66 nfif
109 108 nfel2
110 eqeq1 ${⊢}{k}={m}\to \left({k}={X}↔{m}={X}\right)$
111 csbeq1a
112 69 111 difeq12d
113 110 112 69 ifbieq12d
114 68 113 eleq12d
115 104 109 114 cbvralw
116 91 103 115 3bitr4g ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left(\exists {k}\in {A}\phantom{\rule{.4em}{0ex}}¬{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)↔\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{B}\setminus {C},{B}\right)\right)$
117 19 116 syl5bbr ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left(¬\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{C},{B}\right)↔\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{B}\setminus {C},{B}\right)\right)$
118 18 117 bitrd ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left(¬{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)↔\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{B}\setminus {C},{B}\right)\right)$
119 ibar ${⊢}{z}\in \underset{{k}\in {A}}{⨉}{B}\to \left(¬{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)↔\left({z}\in \underset{{k}\in {A}}{⨉}{B}\wedge ¬{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)\right)\right)$
120 119 adantl ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left(¬{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)↔\left({z}\in \underset{{k}\in {A}}{⨉}{B}\wedge ¬{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)\right)\right)$
121 13 biantrurd ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left(\forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{B}\setminus {C},{B}\right)↔\left({z}Fn{A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{B}\setminus {C},{B}\right)\right)\right)$
122 118 120 121 3bitr3d ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left(\left({z}\in \underset{{k}\in {A}}{⨉}{B}\wedge ¬{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)\right)↔\left({z}Fn{A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{B}\setminus {C},{B}\right)\right)\right)$
123 eldif ${⊢}{z}\in \left(\underset{{k}\in {A}}{⨉}{B}\setminus \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)\right)↔\left({z}\in \underset{{k}\in {A}}{⨉}{B}\wedge ¬{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)\right)$
124 15 elixp ${⊢}{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{B}\setminus {C},{B}\right)↔\left({z}Fn{A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{z}\left({k}\right)\in if\left({k}={X},{B}\setminus {C},{B}\right)\right)$
125 122 123 124 3bitr4g ${⊢}\left(\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\wedge {z}\in \underset{{k}\in {A}}{⨉}{B}\right)\to \left({z}\in \left(\underset{{k}\in {A}}{⨉}{B}\setminus \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)\right)↔{z}\in \underset{{k}\in {A}}{⨉}if\left({k}={X},{B}\setminus {C},{B}\right)\right)$
126 2 11 125 eqrdav ${⊢}\left({X}\in {A}\wedge \forall {k}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\to \underset{{k}\in {A}}{⨉}{B}\setminus \underset{{k}\in {A}}{⨉}if\left({k}={X},{C},{B}\right)=\underset{{k}\in {A}}{⨉}if\left({k}={X},{B}\setminus {C},{B}\right)$