Step | Hyp | Ref
| Expression |
1 | | fveq2 6674 |
. . . 4
⊢ (𝑠 = 𝑡 → (𝐼‘𝑠) = (𝐼‘𝑡)) |
2 | | id 22 |
. . . 4
⊢ (𝑠 = 𝑡 → 𝑠 = 𝑡) |
3 | 1, 2 | sseq12d 3910 |
. . 3
⊢ (𝑠 = 𝑡 → ((𝐼‘𝑠) ⊆ 𝑠 ↔ (𝐼‘𝑡) ⊆ 𝑡)) |
4 | 3 | cbvralvw 3349 |
. 2
⊢
(∀𝑠 ∈
𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐼‘𝑡) ⊆ 𝑡) |
5 | | ntrcls.d |
. . . . 5
⊢ 𝐷 = (𝑂‘𝐵) |
6 | | ntrcls.r |
. . . . 5
⊢ (𝜑 → 𝐼𝐷𝐾) |
7 | 5, 6 | ntrclsrcomplex 41191 |
. . . 4
⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) |
8 | 7 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) |
9 | 5, 6 | ntrclsrcomplex 41191 |
. . . . 5
⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
10 | 9 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵) |
11 | | difeq2 4007 |
. . . . . 6
⊢ (𝑠 = (𝐵 ∖ 𝑡) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑡))) |
12 | 11 | eqeq2d 2749 |
. . . . 5
⊢ (𝑠 = (𝐵 ∖ 𝑡) → (𝑡 = (𝐵 ∖ 𝑠) ↔ 𝑡 = (𝐵 ∖ (𝐵 ∖ 𝑡)))) |
13 | 12 | adantl 485 |
. . . 4
⊢ (((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑡)) → (𝑡 = (𝐵 ∖ 𝑠) ↔ 𝑡 = (𝐵 ∖ (𝐵 ∖ 𝑡)))) |
14 | | elpwi 4497 |
. . . . . . 7
⊢ (𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵) |
15 | | dfss4 4149 |
. . . . . . 7
⊢ (𝑡 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡) |
16 | 14, 15 | sylib 221 |
. . . . . 6
⊢ (𝑡 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡) |
17 | 16 | adantl 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑡)) = 𝑡) |
18 | 17 | eqcomd 2744 |
. . . 4
⊢ ((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵) → 𝑡 = (𝐵 ∖ (𝐵 ∖ 𝑡))) |
19 | 10, 13, 18 | rspcedvd 3529 |
. . 3
⊢ ((𝜑 ∧ 𝑡 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑡 = (𝐵 ∖ 𝑠)) |
20 | | fveq2 6674 |
. . . . . 6
⊢ (𝑡 = (𝐵 ∖ 𝑠) → (𝐼‘𝑡) = (𝐼‘(𝐵 ∖ 𝑠))) |
21 | | id 22 |
. . . . . 6
⊢ (𝑡 = (𝐵 ∖ 𝑠) → 𝑡 = (𝐵 ∖ 𝑠)) |
22 | 20, 21 | sseq12d 3910 |
. . . . 5
⊢ (𝑡 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑡) ⊆ 𝑡 ↔ (𝐼‘(𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ 𝑠))) |
23 | 22 | 3ad2ant3 1136 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐼‘𝑡) ⊆ 𝑡 ↔ (𝐼‘(𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ 𝑠))) |
24 | | ntrcls.o |
. . . . . . . . . . . 12
⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑m 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗)))))) |
25 | 24, 5, 6 | ntrclsiex 41209 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
26 | | elmapi 8459 |
. . . . . . . . . . 11
⊢ (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
27 | 25, 26 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
28 | 27 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
29 | 7 | 3ad2ant1 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵) |
30 | 28, 29 | ffvelrnd 6862 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵) |
31 | 30 | elpwid 4499 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵) |
32 | | difssd 4023 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → (𝐵 ∖ 𝑠) ⊆ 𝐵) |
33 | | sscon34b 4185 |
. . . . . . 7
⊢ (((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∧ (𝐵 ∖ 𝑠) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) |
34 | 31, 32, 33 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) |
35 | | simp2 1138 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → 𝑠 ∈ 𝒫 𝐵) |
36 | | elpwi 4497 |
. . . . . . . . 9
⊢ (𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵) |
37 | | dfss4 4149 |
. . . . . . . . 9
⊢ (𝑠 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑠)) = 𝑠) |
38 | 36, 37 | sylib 221 |
. . . . . . . 8
⊢ (𝑠 ∈ 𝒫 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑠)) = 𝑠) |
39 | 38 | sseq1d 3908 |
. . . . . . 7
⊢ (𝑠 ∈ 𝒫 𝐵 → ((𝐵 ∖ (𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ↔ 𝑠 ⊆ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) |
40 | 35, 39 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐵 ∖ (𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ↔ 𝑠 ⊆ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) |
41 | 34, 40 | bitrd 282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ 𝑠) ↔ 𝑠 ⊆ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) |
42 | 5, 6 | ntrclsbex 41190 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ V) |
43 | 42 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → 𝐵 ∈ V) |
44 | 25 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) |
45 | | eqid 2738 |
. . . . . . 7
⊢ (𝐷‘𝐼) = (𝐷‘𝐼) |
46 | | eqid 2738 |
. . . . . . 7
⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠) |
47 | 24, 5, 43, 44, 45, 35, 46 | dssmapfv3d 41173 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠)))) |
48 | 47 | sseq2d 3909 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → (𝑠 ⊆ ((𝐷‘𝐼)‘𝑠) ↔ 𝑠 ⊆ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))) |
49 | 24, 5, 6 | ntrclsfv1 41211 |
. . . . . . . 8
⊢ (𝜑 → (𝐷‘𝐼) = 𝐾) |
50 | 49 | fveq1d 6676 |
. . . . . . 7
⊢ (𝜑 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠)) |
51 | 50 | sseq2d 3909 |
. . . . . 6
⊢ (𝜑 → (𝑠 ⊆ ((𝐷‘𝐼)‘𝑠) ↔ 𝑠 ⊆ (𝐾‘𝑠))) |
52 | 51 | 3ad2ant1 1134 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → (𝑠 ⊆ ((𝐷‘𝐼)‘𝑠) ↔ 𝑠 ⊆ (𝐾‘𝑠))) |
53 | 41, 48, 52 | 3bitr2d 310 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ (𝐵 ∖ 𝑠) ↔ 𝑠 ⊆ (𝐾‘𝑠))) |
54 | 23, 53 | bitrd 282 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = (𝐵 ∖ 𝑠)) → ((𝐼‘𝑡) ⊆ 𝑡 ↔ 𝑠 ⊆ (𝐾‘𝑠))) |
55 | 8, 19, 54 | ralxfrd2 5279 |
. 2
⊢ (𝜑 → (∀𝑡 ∈ 𝒫 𝐵(𝐼‘𝑡) ⊆ 𝑡 ↔ ∀𝑠 ∈ 𝒫 𝐵𝑠 ⊆ (𝐾‘𝑠))) |
56 | 4, 55 | syl5bb 286 |
1
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 ↔ ∀𝑠 ∈ 𝒫 𝐵𝑠 ⊆ (𝐾‘𝑠))) |