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 ixpfn ⊢ z ∈ ⨉ k ∈ A B → z Fn A
13 12 adantl ⊢ X ∈ A ∧ ∀ k ∈ A C ⊆ B ∧ z ∈ ⨉ k ∈ A B → z Fn A
14 13 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
15 vex ⊢ z ∈ V
16 15 elixp ⊢ z ∈ ⨉ k ∈ A if k = X C B ↔ z Fn A ∧ ∀ k ∈ A z ⁡ k ∈ if k = X C B
17 14 16 syl6rbbr ⊢ 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 15 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 13 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 15 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