Proof of Theorem ntrkbimka
Step | Hyp | Ref
| Expression |
1 | | inidm 4158 |
. 2
⊢ ((𝐼‘∅) ∩ (𝐼‘∅)) = (𝐼‘∅) |
2 | | 0elpw 5282 |
. . 3
⊢ ∅
∈ 𝒫 𝐵 |
3 | | ineq1 4145 |
. . . . . . 7
⊢ (𝑠 = ∅ → (𝑠 ∩ 𝑡) = (∅ ∩ 𝑡)) |
4 | 3 | eqeq1d 2742 |
. . . . . 6
⊢ (𝑠 = ∅ → ((𝑠 ∩ 𝑡) = ∅ ↔ (∅ ∩ 𝑡) = ∅)) |
5 | | fveq2 6771 |
. . . . . . . 8
⊢ (𝑠 = ∅ → (𝐼‘𝑠) = (𝐼‘∅)) |
6 | 5 | ineq1d 4151 |
. . . . . . 7
⊢ (𝑠 = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘∅) ∩ (𝐼‘𝑡))) |
7 | 6 | eqeq1d 2742 |
. . . . . 6
⊢ (𝑠 = ∅ → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘∅) ∩ (𝐼‘𝑡)) = ∅)) |
8 | 4, 7 | imbi12d 345 |
. . . . 5
⊢ (𝑠 = ∅ → (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ((∅ ∩ 𝑡) = ∅ → ((𝐼‘∅) ∩ (𝐼‘𝑡)) = ∅))) |
9 | | 0in 4333 |
. . . . . 6
⊢ (∅
∩ 𝑡) =
∅ |
10 | | pm5.5 362 |
. . . . . 6
⊢ ((∅
∩ 𝑡) = ∅ →
(((∅ ∩ 𝑡) =
∅ → ((𝐼‘∅) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝐼‘∅) ∩ (𝐼‘𝑡)) = ∅)) |
11 | 9, 10 | ax-mp 5 |
. . . . 5
⊢
(((∅ ∩ 𝑡)
= ∅ → ((𝐼‘∅) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝐼‘∅) ∩ (𝐼‘𝑡)) = ∅) |
12 | 8, 11 | bitrdi 287 |
. . . 4
⊢ (𝑠 = ∅ → (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝐼‘∅) ∩ (𝐼‘𝑡)) = ∅)) |
13 | | fveq2 6771 |
. . . . . 6
⊢ (𝑡 = ∅ → (𝐼‘𝑡) = (𝐼‘∅)) |
14 | 13 | ineq2d 4152 |
. . . . 5
⊢ (𝑡 = ∅ → ((𝐼‘∅) ∩ (𝐼‘𝑡)) = ((𝐼‘∅) ∩ (𝐼‘∅))) |
15 | 14 | eqeq1d 2742 |
. . . 4
⊢ (𝑡 = ∅ → (((𝐼‘∅) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘∅) ∩ (𝐼‘∅)) =
∅)) |
16 | 12, 15 | rspc2v 3571 |
. . 3
⊢ ((∅
∈ 𝒫 𝐵 ∧
∅ ∈ 𝒫 𝐵)
→ (∀𝑠 ∈
𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) → ((𝐼‘∅) ∩ (𝐼‘∅)) =
∅)) |
17 | 2, 2, 16 | mp2an 689 |
. 2
⊢
(∀𝑠 ∈
𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) → ((𝐼‘∅) ∩ (𝐼‘∅)) = ∅) |
18 | 1, 17 | eqtr3id 2794 |
1
⊢
(∀𝑠 ∈
𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) → (𝐼‘∅) = ∅) |