| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . . . 5
⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎)) | 
| 2 | 1 | ineq1d 4218 | . . . 4
⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡))) | 
| 3 |  | ineq1 4212 | . . . . 5
⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡)) | 
| 4 | 3 | fveq2d 6909 | . . . 4
⊢ (𝑠 = 𝑎 → (𝐼‘(𝑠 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑡))) | 
| 5 | 2, 4 | sseq12d 4016 | . . 3
⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡)))) | 
| 6 |  | fveq2 6905 | . . . . 5
⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏)) | 
| 7 | 6 | ineq2d 4219 | . . . 4
⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏))) | 
| 8 |  | ineq2 4213 | . . . . 5
⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏)) | 
| 9 | 8 | fveq2d 6909 | . . . 4
⊢ (𝑡 = 𝑏 → (𝐼‘(𝑎 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑏))) | 
| 10 | 7, 9 | sseq12d 4016 | . . 3
⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)))) | 
| 11 | 5, 10 | cbvral2vw 3240 | . 2
⊢
(∀𝑠 ∈
𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏))) | 
| 12 |  | ntrcls.d | . . . . . 6
⊢ 𝐷 = (𝑂‘𝐵) | 
| 13 |  | ntrcls.r | . . . . . 6
⊢ (𝜑 → 𝐼𝐷𝐾) | 
| 14 | 12, 13 | ntrclsbex 44052 | . . . . 5
⊢ (𝜑 → 𝐵 ∈ V) | 
| 15 |  | difssd 4136 | . . . . 5
⊢ (𝜑 → (𝐵 ∖ 𝑠) ⊆ 𝐵) | 
| 16 | 14, 15 | sselpwd 5327 | . . . 4
⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) | 
| 17 | 16 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) | 
| 18 |  | elpwi 4606 | . . . 4
⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵) | 
| 19 |  | simpl 482 | . . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → 𝐵 ∈ V) | 
| 20 |  | difssd 4136 | . . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ⊆ 𝐵) | 
| 21 | 19, 20 | sselpwd 5327 | . . . . 5
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵) | 
| 22 |  | simpr 484 | . . . . . . . 8
⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → 𝑠 = (𝐵 ∖ 𝑎)) | 
| 23 | 22 | difeq2d 4125 | . . . . . . 7
⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎))) | 
| 24 | 23 | eqeq2d 2747 | . . . . . 6
⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)))) | 
| 25 |  | eqcom 2743 | . . . . . 6
⊢ (𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎) | 
| 26 | 24, 25 | bitrdi 287 | . . . . 5
⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)) | 
| 27 |  | dfss4 4268 | . . . . . . 7
⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎) | 
| 28 | 27 | biimpi 216 | . . . . . 6
⊢ (𝑎 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎) | 
| 29 | 28 | adantl 481 | . . . . 5
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎) | 
| 30 | 21, 26, 29 | rspcedvd 3623 | . . . 4
⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠)) | 
| 31 | 14, 18, 30 | syl2an 596 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠)) | 
| 32 |  | simpl1 1191 | . . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑) | 
| 33 |  | difssd 4136 | . . . . . 6
⊢ (𝜑 → (𝐵 ∖ 𝑡) ⊆ 𝐵) | 
| 34 | 14, 33 | sselpwd 5327 | . . . . 5
⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) | 
| 35 | 32, 34 | syl 17 | . . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) | 
| 36 |  | elpwi 4606 | . . . . . 6
⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵) | 
| 37 |  | simpl 482 | . . . . . . . 8
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → 𝐵 ∈ V) | 
| 38 |  | difssd 4136 | . . . . . . . 8
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ⊆ 𝐵) | 
| 39 | 37, 38 | sselpwd 5327 | . . . . . . 7
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵) | 
| 40 |  | simpr 484 | . . . . . . . . . 10
⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → 𝑡 = (𝐵 ∖ 𝑏)) | 
| 41 | 40 | difeq2d 4125 | . . . . . . . . 9
⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏))) | 
| 42 | 41 | eqeq2d 2747 | . . . . . . . 8
⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)))) | 
| 43 |  | eqcom 2743 | . . . . . . . 8
⊢ (𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏) | 
| 44 | 42, 43 | bitrdi 287 | . . . . . . 7
⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)) | 
| 45 |  | dfss4 4268 | . . . . . . . . 9
⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏) | 
| 46 | 45 | biimpi 216 | . . . . . . . 8
⊢ (𝑏 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏) | 
| 47 | 46 | adantl 481 | . . . . . . 7
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏) | 
| 48 | 39, 44, 47 | rspcedvd 3623 | . . . . . 6
⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡)) | 
| 49 | 14, 36, 48 | syl2an 596 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡)) | 
| 50 | 49 | 3ad2antl1 1185 | . . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡)) | 
| 51 |  | simp13 1205 | . . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠)) | 
| 52 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠))) | 
| 53 | 52 | ineq1d 4218 | . . . . . . 7
⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏))) | 
| 54 |  | ineq1 4212 | . . . . . . . 8
⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏)) | 
| 55 | 54 | fveq2d 6909 | . . . . . . 7
⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘(𝑎 ∩ 𝑏)) = (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏))) | 
| 56 | 53, 55 | sseq12d 4016 | . . . . . 6
⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))) | 
| 57 | 51, 56 | syl 17 | . . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))) | 
| 58 |  | fveq2 6905 | . . . . . . . 8
⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡))) | 
| 59 | 58 | ineq2d 4219 | . . . . . . 7
⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) | 
| 60 |  | ineq2 4213 | . . . . . . . . 9
⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))) | 
| 61 |  | difundi 4289 | . . . . . . . . 9
⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)) | 
| 62 | 60, 61 | eqtr4di 2794 | . . . . . . . 8
⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠 ∪ 𝑡))) | 
| 63 | 62 | fveq2d 6909 | . . . . . . 7
⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) | 
| 64 | 59, 63 | sseq12d 4016 | . . . . . 6
⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))) | 
| 65 | 64 | 3ad2ant3 1135 | . . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))) | 
| 66 |  | simp11 1203 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑) | 
| 67 |  | ntrcls.o | . . . . . . . . 9
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗)))))) | 
| 68 | 67, 12, 13 | ntrclsiex 44071 | . . . . . . . 8
⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) | 
| 69 | 68, 14 | jca 511 | . . . . . . 7
⊢ (𝜑 → (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵) ∧ 𝐵 ∈ V)) | 
| 70 |  | elmapi 8890 | . . . . . . . . . . . 12
⊢ (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) | 
| 71 | 70 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) | 
| 72 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → 𝐵 ∈ V) | 
| 73 |  | difssd 4136 | . . . . . . . . . . . 12
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ⊆ 𝐵) | 
| 74 | 72, 73 | sselpwd 5327 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) | 
| 75 | 71, 74 | ffvelcdmd 7104 | . . . . . . . . . 10
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵) | 
| 76 | 75 | elpwid 4608 | . . . . . . . . 9
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵) | 
| 77 |  | orc 867 | . . . . . . . . 9
⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵)) | 
| 78 |  | inss 4247 | . . . . . . . . 9
⊢ (((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵) | 
| 79 | 76, 77, 78 | 3syl 18 | . . . . . . . 8
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵) | 
| 80 |  | difssd 4136 | . . . . . . . . . . 11
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ⊆ 𝐵) | 
| 81 | 72, 80 | sselpwd 5327 | . . . . . . . . . 10
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ∈ 𝒫 𝐵) | 
| 82 | 71, 81 | ffvelcdmd 7104 | . . . . . . . . 9
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ∈ 𝒫 𝐵) | 
| 83 | 82 | elpwid 4608 | . . . . . . . 8
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵) | 
| 84 | 79, 83 | jca 511 | . . . . . . 7
⊢ ((𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) ∧ 𝐵 ∈ V) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵)) | 
| 85 |  | sscon34b 4303 | . . . . . . 7
⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))) | 
| 86 | 66, 69, 84, 85 | 4syl 19 | . . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))))) | 
| 87 |  | difindi 4291 | . . . . . . . 8
⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) | 
| 88 | 87 | sseq2i 4012 | . . . . . . 7
⊢ ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))) | 
| 89 | 88 | a1i 11 | . . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))) | 
| 90 | 66, 14 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝐵 ∈ V) | 
| 91 | 66, 68 | syl 17 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) | 
| 92 |  | simp12 1204 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵) | 
| 93 |  | rp-simp2 43811 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵) | 
| 94 |  | simpl2 1192 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V) | 
| 95 |  | simpl3 1193 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) | 
| 96 |  | eqid 2736 | . . . . . . . . . 10
⊢ (𝐷‘𝐼) = (𝐷‘𝐼) | 
| 97 |  | simpl 482 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V) | 
| 98 |  | simprl 770 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵) | 
| 99 | 98 | elpwid 4608 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ⊆ 𝐵) | 
| 100 |  | simprr 772 | . . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵) | 
| 101 | 100 | elpwid 4608 | . . . . . . . . . . . . 13
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ⊆ 𝐵) | 
| 102 | 99, 101 | unssd 4191 | . . . . . . . . . . . 12
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ⊆ 𝐵) | 
| 103 | 97, 102 | sselpwd 5327 | . . . . . . . . . . 11
⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵) | 
| 104 | 103 | 3ad2antl2 1186 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵) | 
| 105 |  | eqid 2736 | . . . . . . . . . 10
⊢ ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) | 
| 106 | 67, 12, 94, 95, 96, 104, 105 | dssmapfv3d 44037 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))) | 
| 107 |  | simpl1 1191 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝜑) | 
| 108 | 67, 12, 13 | ntrclsfv1 44073 | . . . . . . . . . . 11
⊢ (𝜑 → (𝐷‘𝐼) = 𝐾) | 
| 109 | 108 | fveq1d 6907 | . . . . . . . . . 10
⊢ (𝜑 → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡))) | 
| 110 | 107, 109 | syl 17 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡))) | 
| 111 | 106, 110 | eqtr3d 2778 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐾‘(𝑠 ∪ 𝑡))) | 
| 112 |  | simprl 770 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵) | 
| 113 |  | eqid 2736 | . . . . . . . . . . 11
⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠) | 
| 114 | 67, 12, 94, 95, 96, 112, 113 | dssmapfv3d 44037 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠)))) | 
| 115 | 108 | fveq1d 6907 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠)) | 
| 116 | 107, 115 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠)) | 
| 117 | 114, 116 | eqtr3d 2778 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) = (𝐾‘𝑠)) | 
| 118 |  | simprr 772 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵) | 
| 119 |  | eqid 2736 | . . . . . . . . . . 11
⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡) | 
| 120 | 67, 12, 94, 95, 96, 118, 119 | dssmapfv3d 44037 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) | 
| 121 | 108 | fveq1d 6907 | . . . . . . . . . . 11
⊢ (𝜑 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡)) | 
| 122 | 107, 121 | syl 17 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡)) | 
| 123 | 120, 122 | eqtr3d 2778 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))) = (𝐾‘𝑡)) | 
| 124 | 117, 123 | uneq12d 4168 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡))) | 
| 125 | 111, 124 | sseq12d 4016 | . . . . . . 7
⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) | 
| 126 | 66, 90, 91, 92, 93, 125 | syl32anc 1379 | . . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) | 
| 127 | 86, 89, 126 | 3bitrd 305 | . . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) | 
| 128 | 57, 65, 127 | 3bitrd 305 | . . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) | 
| 129 | 35, 50, 128 | ralxfrd2 5411 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) | 
| 130 | 17, 31, 129 | ralxfrd2 5411 | . 2
⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) | 
| 131 | 11, 130 | bitrid 283 | 1
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))) |