Step | Hyp | Ref
| Expression |
1 | | fveq2 6686 |
. . . . 5
⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎)) |
2 | 1 | ineq1d 4112 |
. . . 4
⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡))) |
3 | | ineq1 4106 |
. . . . 5
⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡)) |
4 | 3 | fveq2d 6690 |
. . . 4
⊢ (𝑠 = 𝑎 → (𝐼‘(𝑠 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑡))) |
5 | 2, 4 | sseq12d 3920 |
. . 3
⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡)))) |
6 | | fveq2 6686 |
. . . . 5
⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏)) |
7 | 6 | ineq2d 4113 |
. . . 4
⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏))) |
8 | | ineq2 4107 |
. . . . 5
⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏)) |
9 | 8 | fveq2d 6690 |
. . . 4
⊢ (𝑡 = 𝑏 → (𝐼‘(𝑎 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑏))) |
10 | 7, 9 | sseq12d 3920 |
. . 3
⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)))) |
11 | 5, 10 | cbvral2vw 3363 |
. 2
⊢
(∀𝑠 ∈
𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏))) |
12 | | ntrcls.d |
. . . . . 6
⊢ 𝐷 = (𝑂‘𝐵) |
13 | | ntrcls.r |
. . . . . 6
⊢ (𝜑 → 𝐼𝐷𝐾) |
14 | 12, 13 | ntrclsbex 41230 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ V) |
15 | | difssd 4033 |
. . . . 5
⊢ (𝜑 → (𝐵 ∖ 𝑠) ⊆ 𝐵) |
16 | 14, 15 | sselpwd 5204 |
. . . 4
⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) |
17 | 16 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) |
18 | | elpwi 4507 |
. . . 4
⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵) |
19 | | simpl 486 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → 𝐵 ∈ V) |
20 | | difssd 4033 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ⊆ 𝐵) |
21 | 19, 20 | sselpwd 5204 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵) |
22 | | simpr 488 |
. . . . . . . 8
⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → 𝑠 = (𝐵 ∖ 𝑎)) |
23 | 22 | difeq2d 4023 |
. . . . . . 7
⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎))) |
24 | 23 | eqeq2d 2750 |
. . . . . 6
⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))) |
25 | | eqcom 2746 |
. . . . . 6
⊢ (𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎) |
26 | 24, 25 | bitrdi 290 |
. . . . 5
⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)) |
27 | | dfss4 4159 |
. . . . . . 7
⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎) |
28 | 27 | biimpi 219 |
. . . . . 6
⊢ (𝑎 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎) |
29 | 28 | adantl 485 |
. . . . 5
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎) |
30 | 21, 26, 29 | rspcedvd 3532 |
. . . 4
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠)) |
31 | 14, 18, 30 | syl2an 599 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠)) |
32 | | simpl1 1192 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑) |
33 | | difssd 4033 |
. . . . . 6
⊢ (𝜑 → (𝐵 ∖ 𝑡) ⊆ 𝐵) |
34 | 14, 33 | sselpwd 5204 |
. . . . 5
⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
35 | 32, 34 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
36 | | elpwi 4507 |
. . . . . 6
⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵) |
37 | | simpl 486 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → 𝐵 ∈ V) |
38 | | difssd 4033 |
. . . . . . . 8
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ⊆ 𝐵) |
39 | 37, 38 | sselpwd 5204 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵) |
40 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → 𝑡 = (𝐵 ∖ 𝑏)) |
41 | 40 | difeq2d 4023 |
. . . . . . . . 9
⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏))) |
42 | 41 | eqeq2d 2750 |
. . . . . . . 8
⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))) |
43 | | eqcom 2746 |
. . . . . . . 8
⊢ (𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏) |
44 | 42, 43 | bitrdi 290 |
. . . . . . 7
⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)) |
45 | | dfss4 4159 |
. . . . . . . . 9
⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏) |
46 | 45 | biimpi 219 |
. . . . . . . 8
⊢ (𝑏 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏) |
47 | 46 | adantl 485 |
. . . . . . 7
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏) |
48 | 39, 44, 47 | rspcedvd 3532 |
. . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡)) |
49 | 14, 36, 48 | syl2an 599 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡)) |
50 | 49 | 3ad2antl1 1186 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡)) |
51 | | simp13 1206 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠)) |
52 | | fveq2 6686 |
. . . . . . . 8
⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠))) |
53 | 52 | ineq1d 4112 |
. . . . . . 7
⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))) |
54 | | ineq1 4106 |
. . . . . . . 8
⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏)) |
55 | 54 | fveq2d 6690 |
. . . . . . 7
⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘(𝑎 ∩ 𝑏)) = (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏))) |
56 | 53, 55 | sseq12d 3920 |
. . . . . 6
⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))) |
57 | 51, 56 | syl 17 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))) |
58 | | fveq2 6686 |
. . . . . . . 8
⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡))) |
59 | 58 | ineq2d 4113 |
. . . . . . 7
⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) |
60 | | ineq2 4107 |
. . . . . . . . 9
⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))) |
61 | | difundi 4180 |
. . . . . . . . 9
⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) |
62 | 60, 61 | eqtr4di 2792 |
. . . . . . . 8
⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠 ∪ 𝑡))) |
63 | 62 | fveq2d 6690 |
. . . . . . 7
⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) |
64 | 59, 63 | sseq12d 3920 |
. . . . . 6
⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))) |
65 | 64 | 3ad2ant3 1136 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))) |
66 | | simp11 1204 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑) |
67 | | ntrcls.o |
. . . . . . . . . 10
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗)))))) |
68 | 67, 12, 13 | ntrclsiex 41249 |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
69 | 68, 14 | jca 515 |
. . . . . . . 8
⊢ (𝜑 → (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝐵 ∈ V)) |
70 | 66, 69 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝐵 ∈ V)) |
71 | | elmapi 8471 |
. . . . . . . . . . . 12
⊢ (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
72 | 71 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
73 | | simpr 488 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → 𝐵 ∈ V) |
74 | | difssd 4033 |
. . . . . . . . . . . 12
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ⊆ 𝐵) |
75 | 73, 74 | sselpwd 5204 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) |
76 | 72, 75 | ffvelrnd 6874 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵) |
77 | 76 | elpwid 4509 |
. . . . . . . . 9
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵) |
78 | | orc 866 |
. . . . . . . . 9
⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵)) |
79 | | inss 4139 |
. . . . . . . . 9
⊢ (((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵) |
80 | 77, 78, 79 | 3syl 18 |
. . . . . . . 8
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵) |
81 | | difssd 4033 |
. . . . . . . . . . 11
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ⊆ 𝐵) |
82 | 73, 81 | sselpwd 5204 |
. . . . . . . . . 10
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ∈ 𝒫 𝐵) |
83 | 72, 82 | ffvelrnd 6874 |
. . . . . . . . 9
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ∈ 𝒫 𝐵) |
84 | 83 | elpwid 4509 |
. . . . . . . 8
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵) |
85 | 80, 84 | jca 515 |
. . . . . . 7
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵)) |
86 | | sscon34b 4195 |
. . . . . . 7
⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))) |
87 | 70, 85, 86 | 3syl 18 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))) |
88 | | difindi 4182 |
. . . . . . . 8
⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) |
89 | 88 | sseq2i 3916 |
. . . . . . 7
⊢ ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))) |
90 | 89 | a1i 11 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))) |
91 | 66, 14 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝐵 ∈ V) |
92 | 66, 68 | syl 17 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
93 | | simp12 1205 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵) |
94 | | rp-simp2 40987 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵) |
95 | | simpl2 1193 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V) |
96 | | simpl3 1194 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
97 | | eqid 2739 |
. . . . . . . . . 10
⊢ (𝐷‘𝐼) = (𝐷‘𝐼) |
98 | | simpl 486 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V) |
99 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵) |
100 | 99 | elpwid 4509 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ⊆ 𝐵) |
101 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵) |
102 | 101 | elpwid 4509 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ⊆ 𝐵) |
103 | 100, 102 | unssd 4086 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ⊆ 𝐵) |
104 | 98, 103 | sselpwd 5204 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵) |
105 | 104 | 3ad2antl2 1187 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵) |
106 | | eqid 2739 |
. . . . . . . . . 10
⊢ ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) |
107 | 67, 12, 95, 96, 97, 105, 106 | dssmapfv3d 41213 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))) |
108 | | simpl1 1192 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝜑) |
109 | 67, 12, 13 | ntrclsfv1 41251 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐷‘𝐼) = 𝐾) |
110 | 109 | fveq1d 6688 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡))) |
111 | 108, 110 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡))) |
112 | 107, 111 | eqtr3d 2776 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐾‘(𝑠 ∪ 𝑡))) |
113 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵) |
114 | | eqid 2739 |
. . . . . . . . . . 11
⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠) |
115 | 67, 12, 95, 96, 97, 113, 114 | dssmapfv3d 41213 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠)))) |
116 | 109 | fveq1d 6688 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠)) |
117 | 108, 116 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠)) |
118 | 115, 117 | eqtr3d 2776 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) = (𝐾‘𝑠)) |
119 | | simprr 773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵) |
120 | | eqid 2739 |
. . . . . . . . . . 11
⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡) |
121 | 67, 12, 95, 96, 97, 119, 120 | dssmapfv3d 41213 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) |
122 | 109 | fveq1d 6688 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡)) |
123 | 108, 122 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡)) |
124 | 121, 123 | eqtr3d 2776 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))) = (𝐾‘𝑡)) |
125 | 118, 124 | uneq12d 4064 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))) |
126 | 112, 125 | sseq12d 3920 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) |
127 | 66, 91, 92, 93, 94, 126 | syl32anc 1379 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) |
128 | 87, 90, 127 | 3bitrd 308 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) |
129 | 57, 65, 128 | 3bitrd 308 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) |
130 | 35, 50, 129 | ralxfrd2 5289 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) |
131 | 17, 31, 130 | ralxfrd2 5289 |
. 2
⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) |
132 | 11, 131 | syl5bb 286 |
1
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) |