| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2fveq3 6911 | . . . 4
⊢ (𝑠 = 𝑡 → (𝐼‘(𝐼‘𝑠)) = (𝐼‘(𝐼‘𝑡))) | 
| 2 |  | fveq2 6906 | . . . 4
⊢ (𝑠 = 𝑡 → (𝐼‘𝑠) = (𝐼‘𝑡)) | 
| 3 | 1, 2 | eqeq12d 2753 | . . 3
⊢ (𝑠 = 𝑡 → ((𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ (𝐼‘(𝐼‘𝑡)) = (𝐼‘𝑡))) | 
| 4 | 3 | cbvralvw 3237 | . 2
⊢
(∀𝑠 ∈
𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑡)) = (𝐼‘𝑡)) | 
| 5 |  | ntrcls.d | . . . . 5
⊢ 𝐷 = (𝑂‘𝐵) | 
| 6 |  | ntrcls.r | . . . . 5
⊢ (𝜑 → 𝐼𝐷𝐾) | 
| 7 | 5, 6 | ntrclsrcomplex 44048 | . . . 4
⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) | 
| 8 | 7 | adantr 480 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) | 
| 9 | 5, 6 | ntrclsrcomplex 44048 | . . . . 5
⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) | 
| 10 | 9 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) | 
| 11 |  | difeq2 4120 | . . . . . 6
⊢ (𝑠 = (𝐵 ∖ 𝑡) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑡))) | 
| 12 | 11 | eqeq2d 2748 | . . . . 5
⊢ (𝑠 = (𝐵 ∖ 𝑡) → (𝑡 = (𝐵 ∖ 𝑠) ↔ 𝑡 = (𝐵 ∖ (𝐵 ∖ 𝑡)))) | 
| 13 | 12 | adantl 481 | . . . 4
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑡)) → (𝑡 = (𝐵 ∖ 𝑠) ↔ 𝑡 = (𝐵 ∖ (𝐵 ∖ 𝑡)))) | 
| 14 |  | elpwi 4607 | . . . . . . 7
⊢ (𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵) | 
| 15 |  | dfss4 4269 | . . . . . . 7
⊢ (𝑡 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡) | 
| 16 | 14, 15 | sylib 218 | . . . . . 6
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡) | 
| 17 | 16 | eqcomd 2743 | . . . . 5
⊢ (𝑡 ∈ 𝒫 𝐵 → 𝑡 = (𝐵 ∖ (𝐵 ∖ 𝑡))) | 
| 18 | 17 | adantl 481 | . . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 = (𝐵 ∖ (𝐵 ∖ 𝑡))) | 
| 19 | 10, 13, 18 | rspcedvd 3624 | . . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑡 = (𝐵 ∖ 𝑠)) | 
| 20 |  | 2fveq3 6911 | . . . . . 6
⊢ (𝑡 = (𝐵 ∖ 𝑠) → (𝐼‘(𝐼‘𝑡)) = (𝐼‘(𝐼‘(𝐵 ∖ 𝑠)))) | 
| 21 |  | fveq2 6906 | . . . . . 6
⊢ (𝑡 = (𝐵 ∖ 𝑠) → (𝐼‘𝑡) = (𝐼‘(𝐵 ∖ 𝑠))) | 
| 22 | 20, 21 | eqeq12d 2753 | . . . . 5
⊢ (𝑡 = (𝐵 ∖ 𝑠) → ((𝐼‘(𝐼‘𝑡)) = (𝐼‘𝑡) ↔ (𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) = (𝐼‘(𝐵 ∖ 𝑠)))) | 
| 23 | 22 | 3ad2ant3 1136 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐼‘(𝐼‘𝑡)) = (𝐼‘𝑡) ↔ (𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) = (𝐼‘(𝐵 ∖ 𝑠)))) | 
| 24 |  | ntrcls.o | . . . . . . . . . . . 12
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗)))))) | 
| 25 | 24, 5, 6 | ntrclsiex 44066 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) | 
| 26 |  | elmapi 8889 | . . . . . . . . . . 11
⊢ (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) | 
| 27 | 25, 26 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵) | 
| 28 | 27, 7 | ffvelcdmd 7105 | . . . . . . . . . 10
⊢ (𝜑 → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵) | 
| 29 | 27, 28 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ (𝜑 → (𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) ∈ 𝒫 𝐵) | 
| 30 | 29 | elpwid 4609 | . . . . . . . 8
⊢ (𝜑 → (𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) ⊆ 𝐵) | 
| 31 | 28 | elpwid 4609 | . . . . . . . 8
⊢ (𝜑 → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵) | 
| 32 |  | rcompleq 4305 | . . . . . . . 8
⊢ (((𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵) → ((𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) = (𝐼‘(𝐵 ∖ 𝑠)) ↔ (𝐵 ∖ (𝐼‘(𝐼‘(𝐵 ∖ 𝑠)))) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) | 
| 33 | 30, 31, 32 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → ((𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) = (𝐼‘(𝐵 ∖ 𝑠)) ↔ (𝐵 ∖ (𝐼‘(𝐼‘(𝐵 ∖ 𝑠)))) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) | 
| 34 | 33 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) = (𝐼‘(𝐵 ∖ 𝑠)) ↔ (𝐵 ∖ (𝐼‘(𝐼‘(𝐵 ∖ 𝑠)))) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) | 
| 35 | 24, 5, 6 | ntrclsnvobr 44065 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾𝐷𝐼) | 
| 36 | 35 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → 𝐾𝐷𝐼) | 
| 37 | 24, 5, 35 | ntrclsiex 44066 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) | 
| 38 |  | elmapi 8889 | . . . . . . . . . . 11
⊢ (𝐾 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝐾:𝒫 𝐵⟶𝒫 𝐵) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → 𝐾:𝒫 𝐵⟶𝒫 𝐵) | 
| 40 | 39 | ffvelcdmda 7104 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐾‘𝑠) ∈ 𝒫 𝐵) | 
| 41 | 24, 5, 36, 40 | ntrclsfv 44072 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐾‘(𝐾‘𝑠)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝐾‘𝑠))))) | 
| 42 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → 𝑠 ∈ 𝒫 𝐵) | 
| 43 | 24, 5, 36, 42 | ntrclsfv 44072 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐾‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠)))) | 
| 44 | 43 | difeq2d 4126 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐾‘𝑠)) = (𝐵 ∖ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) | 
| 45 |  | dfss4 4269 | . . . . . . . . . . . . 13
⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠)))) = (𝐼‘(𝐵 ∖ 𝑠))) | 
| 46 | 31, 45 | sylib 218 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝐵 ∖ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠)))) = (𝐼‘(𝐵 ∖ 𝑠))) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠)))) = (𝐼‘(𝐵 ∖ 𝑠))) | 
| 48 | 44, 47 | eqtrd 2777 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐾‘𝑠)) = (𝐼‘(𝐵 ∖ 𝑠))) | 
| 49 | 48 | fveq2d 6910 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐼‘(𝐵 ∖ (𝐾‘𝑠))) = (𝐼‘(𝐼‘(𝐵 ∖ 𝑠)))) | 
| 50 | 49 | difeq2d 4126 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝐾‘𝑠)))) = (𝐵 ∖ (𝐼‘(𝐼‘(𝐵 ∖ 𝑠))))) | 
| 51 | 41, 50 | eqtrd 2777 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐾‘(𝐾‘𝑠)) = (𝐵 ∖ (𝐼‘(𝐼‘(𝐵 ∖ 𝑠))))) | 
| 52 | 51, 43 | eqeq12d 2753 | . . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠) ↔ (𝐵 ∖ (𝐼‘(𝐼‘(𝐵 ∖ 𝑠)))) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) | 
| 53 | 34, 52 | bitr4d 282 | . . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → ((𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) = (𝐼‘(𝐵 ∖ 𝑠)) ↔ (𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠))) | 
| 54 | 53 | 3adant3 1133 | . . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐼‘(𝐼‘(𝐵 ∖ 𝑠))) = (𝐼‘(𝐵 ∖ 𝑠)) ↔ (𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠))) | 
| 55 | 23, 54 | bitrd 279 | . . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐼‘(𝐼‘𝑡)) = (𝐼‘𝑡) ↔ (𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠))) | 
| 56 | 8, 19, 55 | ralxfrd2 5412 | . 2
⊢ (𝜑 → (∀𝑡 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑡)) = (𝐼‘𝑡) ↔ ∀𝑠 ∈ 𝒫 𝐵(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠))) | 
| 57 | 4, 56 | bitrid 283 | 1
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘(𝐼‘𝑠)) = (𝐼‘𝑠) ↔ ∀𝑠 ∈ 𝒫 𝐵(𝐾‘(𝐾‘𝑠)) = (𝐾‘𝑠))) |