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 A C B k A B k A if k = X C B = k A if k = X B C B

Proof

Step Hyp Ref Expression
1 eldifi z k A B k A if k = X C B z k A B
2 1 adantl X A k A C B z k A B k A if k = X C B z k A B
3 sseq1 B C = if k = X B C B B C B if k = X B C B B
4 sseq1 B = if k = X B C B B B if k = X B C B B
5 difss B C B
6 ssid B B
7 3 4 5 6 keephyp if k = X B C B B
8 7 rgenw k A if k = X B C B B
9 ss2ixp k A if k = X B C B B k A if k = X B C B k A B
10 8 9 mp1i X A k A C B k A if k = X B C B k A B
11 10 sselda X A k A C B z k A if k = X B C B z k A B
12 vex z V
13 12 elixp z k A if k = X C B z Fn A k A z k if k = X C B
14 ixpfn z k A B z Fn A
15 14 adantl X A k A C B z k A B z Fn A
16 15 biantrurd X A k A C B z k A B k A z k if k = X C B z Fn A k A z k if k = X C B
17 13 16 bitr4id X A k A C B z k A B z k A if k = X C B k A z k if k = X C B
18 17 notbid X A k A C B z k A B ¬ z k A if k = X C B ¬ k A z k if k = X C B
19 rexnal k A ¬ z k if k = X C B ¬ k A z k if k = X C B
20 eleq2 m / k B m / k C = if m = X m / k B m / k C m / k B z m m / k B m / k C z m if m = X m / k B m / k C m / k B
21 eleq2 m / k B = if m = X m / k B m / k C m / k B z m m / k B z m if m = X m / k B m / k C m / k B
22 eleq2 l / k C = if l = X l / k C l / k B z l l / k C z l if l = X l / k C l / k B
23 eleq2 l / k B = if l = X l / k C l / k B z l l / k B z l if l = X l / k C l / k B
24 simpl X A k A C B X A
25 12 elixp z k A B z Fn A k A z k B
26 25 simprbi z k A B k A z k B
27 nfv l z k B
28 nfcsb1v _ k l / k B
29 28 nfel2 k z 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 A z k B l A z l l / k B
34 26 33 sylib z k A B l A z 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 A z l l / k B z X X / k B
39 24 34 38 syl2an X A k A C B z k A B 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 A C B z k A B ¬ z X X / k B X / k C z X X / k C
42 41 adantr X A k A C B z k A B ¬ 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 A C B z k A B ¬ z X X / k B X / k C l A l = X z l l / k C
46 45 imp X A k A C B z k A B ¬ z X X / k B X / k C l A l = X z l l / k C
47 34 ad2antlr X A k A C B z k A B ¬ z X X / k B X / k C l A z l l / k B
48 47 r19.21bi X A k A C B z k A B ¬ z X X / k B X / k C l A z l l / k B
49 48 adantr X A k A C B z k A B ¬ 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 A C B z k A B ¬ z X X / k B X / k C l A z l if l = X l / k C l / k B
51 50 ralrimiva X A k A C B z k A B ¬ z X X / k B X / k C l A z l if l = X l / k C l / k B
52 dfral2 l A z l if l = X l / k C l / k B ¬ l A ¬ z l if l = X l / k C l / k B
53 51 52 sylib X A k A C B z k A B ¬ z X X / k B X / k C ¬ l A ¬ z l if l = X l / k C l / k B
54 53 ex X A k A C B z k A B ¬ z X X / k B X / k C ¬ l A ¬ z l if l = X l / k C l / k B
55 54 con4d X A k A C B z k A B l A ¬ z l if l = X l / k C l / k B z X X / k B X / k C
56 55 imp X A k A C B z k A B l A ¬ z l if l = X l / k C l / k B z X X / k B X / k C
57 56 adantr X A k A C B z k A B l A ¬ z l if l = 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 A C B z k A B l A ¬ z l if l = 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 A C B z k A B l A ¬ z l if l = X l / k C l / k B m A m = X z m m / k B m / k C
65 nfv m z k B
66 nfcsb1v _ k m / k B
67 66 nfel2 k z 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 A z k B m A z m m / k B
72 26 71 sylib z k A B m A z m m / k B
73 72 ad2antlr X A k A C B z k A B l A ¬ z l if l = X l / k C l / k B m A z m m / k B
74 73 r19.21bi X A k A C B z k A B l A ¬ z l if l = X l / k C l / k B m A z m m / k B
75 74 adantr X A k A C B z k A B l A ¬ z l if l = 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 A C B z k A B l A ¬ z l if l = X l / k C l / k B m A z m if m = X m / k B m / k C m / k B
77 76 ralrimiva X A k A C B z k A B l A ¬ z l if l = X l / k C l / k B m A z m if m = X m / k B m / k C m / k B
78 simpll X A k A C B z k A B X A
79 iftrue m = X if m = X m / k B m / k C m / k B = m / k B m / k C
80 79 61 eqtrd m = X if m = X m / k B m / k C m / k B = X / k B X / k C
81 58 80 eleq12d m = X z m if m = X m / k B m / k C m / k B z X X / k B X / k C
82 81 rspcva X A m A z m if m = 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 A C B z k A B m A z m if m = X m / k B m / k C m / k B z X X / k B X / k C
84 83 eldifbd X A k A C B z k A B m A z m if m = X m / k B m / k C m / k B ¬ z X X / k C
85 iftrue l = X if l = X l / k C l / k B = l / k C
86 85 43 eqtrd l = X if l = X l / k C l / k B = X / k C
87 35 86 eleq12d l = X z l if l = X l / k C l / k B z X X / k C
88 87 notbid l = X ¬ z l if l = 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 if l = X l / k C l / k B
90 78 84 89 syl2an2r X A k A C B z k A B m A z m if m = X m / k B m / k C m / k B l A ¬ z l if l = X l / k C l / k B
91 77 90 impbida X A k A C B z k A B l A ¬ z l if l = X l / k C l / k B m A z m if m = X m / k B m / k C m / k B
92 nfv l ¬ z k if k = X C B
93 nfv k l = X
94 nfcsb1v _ k l / k C
95 93 94 28 nfif _ k if l = X l / k C l / k B
96 95 nfel2 k z l if l = X l / k C l / k B
97 96 nfn k ¬ z l if l = 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 if k = X C B = if l = X l / k C l / k B
101 30 100 eleq12d k = l z k if k = X C B z l if l = X l / k C l / k B
102 101 notbid k = l ¬ z k if k = X C B ¬ z l if l = X l / k C l / k B
103 92 97 102 cbvrexw k A ¬ z k if k = X C B l A ¬ z l if l = X l / k C l / k B
104 nfv m z k if k = X B C B
105 nfv k m = X
106 nfcsb1v _ k m / k C
107 66 106 nfdif _ k m / k B m / k C
108 105 107 66 nfif _ k if m = X m / k B m / k C m / k B
109 108 nfel2 k z m if m = 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 if k = X B C B = if m = X m / k B m / k C m / k B
114 68 113 eleq12d k = m z k if k = X B C B z m if m = X m / k B m / k C m / k B
115 104 109 114 cbvralw k A z k if k = X B C B m A z m if m = X m / k B m / k C m / k B
116 91 103 115 3bitr4g X A k A C B z k A B k A ¬ z k if k = X C B k A z k if k = X B C B
117 19 116 bitr3id X A k A C B z k A B ¬ k A z k if k = X C B k A z k if k = X B C B
118 18 117 bitrd X A k A C B z k A B ¬ z k A if k = X C B k A z k if k = X B C B
119 ibar z k A B ¬ z k A if k = X C B z k A B ¬ z k A if k = X C B
120 119 adantl X A k A C B z k A B ¬ z k A if k = X C B z k A B ¬ z k A if k = X C B
121 15 biantrurd X A k A C B z k A B k A z k if k = X B C B z Fn A k A z k if k = X B C B
122 118 120 121 3bitr3d X A k A C B z k A B z k A B ¬ z k A if k = X C B z Fn A k A z k if k = X B C B
123 eldif z k A B k A if k = X C B z k A B ¬ z k A if k = X C B
124 12 elixp z k A if k = X B C B z Fn A k A z k if k = X B C B
125 122 123 124 3bitr4g X A k A C B z k A B z k A B k A if k = X C B z k A if k = X B C B
126 2 11 125 eqrdav X A k A C B k A B k A if k = X C B = k A if k = X B C B