Proof of Theorem ntrk2imkb
Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . 3
⊢
(∀𝑠 ∈
𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 → ∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠) |
2 | | fveq2 6774 |
. . . . . 6
⊢ (𝑠 = 𝑡 → (𝐼‘𝑠) = (𝐼‘𝑡)) |
3 | | id 22 |
. . . . . 6
⊢ (𝑠 = 𝑡 → 𝑠 = 𝑡) |
4 | 2, 3 | sseq12d 3954 |
. . . . 5
⊢ (𝑠 = 𝑡 → ((𝐼‘𝑠) ⊆ 𝑠 ↔ (𝐼‘𝑡) ⊆ 𝑡)) |
5 | 4 | cbvralvw 3383 |
. . . 4
⊢
(∀𝑠 ∈
𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐼‘𝑡) ⊆ 𝑡) |
6 | 5 | biimpi 215 |
. . 3
⊢
(∀𝑠 ∈
𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 → ∀𝑡 ∈ 𝒫 𝐵(𝐼‘𝑡) ⊆ 𝑡) |
7 | | raaanv 4452 |
. . 3
⊢
(∀𝑠 ∈
𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ⊆ 𝑠 ∧ (𝐼‘𝑡) ⊆ 𝑡) ↔ (∀𝑠 ∈ 𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 ∧ ∀𝑡 ∈ 𝒫 𝐵(𝐼‘𝑡) ⊆ 𝑡)) |
8 | 1, 6, 7 | sylanbrc 583 |
. 2
⊢
(∀𝑠 ∈
𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 → ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ⊆ 𝑠 ∧ (𝐼‘𝑡) ⊆ 𝑡)) |
9 | | ss2in 4170 |
. . . . . . 7
⊢ (((𝐼‘𝑠) ⊆ 𝑠 ∧ (𝐼‘𝑡) ⊆ 𝑡) → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝑠 ∩ 𝑡)) |
10 | 9 | adantr 481 |
. . . . . 6
⊢ ((((𝐼‘𝑠) ⊆ 𝑠 ∧ (𝐼‘𝑡) ⊆ 𝑡) ∧ (𝑠 ∩ 𝑡) = ∅) → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝑠 ∩ 𝑡)) |
11 | | simpr 485 |
. . . . . 6
⊢ ((((𝐼‘𝑠) ⊆ 𝑠 ∧ (𝐼‘𝑡) ⊆ 𝑡) ∧ (𝑠 ∩ 𝑡) = ∅) → (𝑠 ∩ 𝑡) = ∅) |
12 | 10, 11 | sseqtrd 3961 |
. . . . 5
⊢ ((((𝐼‘𝑠) ⊆ 𝑠 ∧ (𝐼‘𝑡) ⊆ 𝑡) ∧ (𝑠 ∩ 𝑡) = ∅) → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ ∅) |
13 | | ss0 4332 |
. . . . 5
⊢ (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ ((((𝐼‘𝑠) ⊆ 𝑠 ∧ (𝐼‘𝑡) ⊆ 𝑡) ∧ (𝑠 ∩ 𝑡) = ∅) → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) |
15 | 14 | ex 413 |
. . 3
⊢ (((𝐼‘𝑠) ⊆ 𝑠 ∧ (𝐼‘𝑡) ⊆ 𝑡) → ((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) |
16 | 15 | 2ralimi 3088 |
. 2
⊢
(∀𝑠 ∈
𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ⊆ 𝑠 ∧ (𝐼‘𝑡) ⊆ 𝑡) → ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) |
17 | 8, 16 | syl 17 |
1
⊢
(∀𝑠 ∈
𝒫 𝐵(𝐼‘𝑠) ⊆ 𝑠 → ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) |