Proof of Theorem ntrk0kbimka
| Step | Hyp | Ref
| Expression |
| 1 | | pwidg 4620 |
. . . . 5
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵) |
| 2 | 1 | ad2antrr 726 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ ((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅))) → 𝐵 ∈ 𝒫 𝐵) |
| 3 | | 0elpw 5356 |
. . . . 5
⊢ ∅
∈ 𝒫 𝐵 |
| 4 | 3 | a1i 11 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ ((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅))) → ∅ ∈
𝒫 𝐵) |
| 5 | | simprr 773 |
. . . 4
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ ((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅))) → ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) |
| 6 | | ineq1 4213 |
. . . . . . 7
⊢ (𝑠 = 𝐵 → (𝑠 ∩ 𝑡) = (𝐵 ∩ 𝑡)) |
| 7 | 6 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑠 = 𝐵 → ((𝑠 ∩ 𝑡) = ∅ ↔ (𝐵 ∩ 𝑡) = ∅)) |
| 8 | | fveq2 6906 |
. . . . . . . 8
⊢ (𝑠 = 𝐵 → (𝐼‘𝑠) = (𝐼‘𝐵)) |
| 9 | 8 | ineq1d 4219 |
. . . . . . 7
⊢ (𝑠 = 𝐵 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝐵) ∩ (𝐼‘𝑡))) |
| 10 | 9 | eqeq1d 2739 |
. . . . . 6
⊢ (𝑠 = 𝐵 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝐵) ∩ (𝐼‘𝑡)) = ∅)) |
| 11 | 7, 10 | imbi12d 344 |
. . . . 5
⊢ (𝑠 = 𝐵 → (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝐵 ∩ 𝑡) = ∅ → ((𝐼‘𝐵) ∩ (𝐼‘𝑡)) = ∅))) |
| 12 | | ineq2 4214 |
. . . . . . . 8
⊢ (𝑡 = ∅ → (𝐵 ∩ 𝑡) = (𝐵 ∩ ∅)) |
| 13 | 12 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑡 = ∅ → ((𝐵 ∩ 𝑡) = ∅ ↔ (𝐵 ∩ ∅) = ∅)) |
| 14 | | fveq2 6906 |
. . . . . . . . 9
⊢ (𝑡 = ∅ → (𝐼‘𝑡) = (𝐼‘∅)) |
| 15 | 14 | ineq2d 4220 |
. . . . . . . 8
⊢ (𝑡 = ∅ → ((𝐼‘𝐵) ∩ (𝐼‘𝑡)) = ((𝐼‘𝐵) ∩ (𝐼‘∅))) |
| 16 | 15 | eqeq1d 2739 |
. . . . . . 7
⊢ (𝑡 = ∅ → (((𝐼‘𝐵) ∩ (𝐼‘𝑡)) = ∅ ↔ ((𝐼‘𝐵) ∩ (𝐼‘∅)) =
∅)) |
| 17 | 13, 16 | imbi12d 344 |
. . . . . 6
⊢ (𝑡 = ∅ → (((𝐵 ∩ 𝑡) = ∅ → ((𝐼‘𝐵) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝐵 ∩ ∅) = ∅ → ((𝐼‘𝐵) ∩ (𝐼‘∅)) =
∅))) |
| 18 | | in0 4395 |
. . . . . . 7
⊢ (𝐵 ∩ ∅) =
∅ |
| 19 | | pm5.5 361 |
. . . . . . 7
⊢ ((𝐵 ∩ ∅) = ∅ →
(((𝐵 ∩ ∅) =
∅ → ((𝐼‘𝐵) ∩ (𝐼‘∅)) = ∅) ↔ ((𝐼‘𝐵) ∩ (𝐼‘∅)) =
∅)) |
| 20 | 18, 19 | mp1i 13 |
. . . . . 6
⊢ (𝑡 = ∅ → (((𝐵 ∩ ∅) = ∅ →
((𝐼‘𝐵) ∩ (𝐼‘∅)) = ∅) ↔ ((𝐼‘𝐵) ∩ (𝐼‘∅)) =
∅)) |
| 21 | 17, 20 | bitrd 279 |
. . . . 5
⊢ (𝑡 = ∅ → (((𝐵 ∩ 𝑡) = ∅ → ((𝐼‘𝐵) ∩ (𝐼‘𝑡)) = ∅) ↔ ((𝐼‘𝐵) ∩ (𝐼‘∅)) =
∅)) |
| 22 | 11, 21 | rspc2va 3634 |
. . . 4
⊢ (((𝐵 ∈ 𝒫 𝐵 ∧ ∅ ∈ 𝒫
𝐵) ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) → ((𝐼‘𝐵) ∩ (𝐼‘∅)) = ∅) |
| 23 | 2, 4, 5, 22 | syl21anc 838 |
. . 3
⊢ (((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) ∧ ((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅))) → ((𝐼‘𝐵) ∩ (𝐼‘∅)) = ∅) |
| 24 | 23 | ex 412 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → (((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) → ((𝐼‘𝐵) ∩ (𝐼‘∅)) =
∅)) |
| 25 | | elmapi 8889 |
. . . . . 6
⊢ (𝐼 ∈ (𝒫 𝐵 ↑m 𝒫
𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
| 26 | 25 | adantl 481 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
| 27 | 3 | a1i 11 |
. . . . 5
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → ∅ ∈
𝒫 𝐵) |
| 28 | 26, 27 | ffvelcdmd 7105 |
. . . 4
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → (𝐼‘∅) ∈ 𝒫 𝐵) |
| 29 | 28 | elpwid 4609 |
. . 3
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → (𝐼‘∅) ⊆ 𝐵) |
| 30 | | simpl 482 |
. . 3
⊢ (((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) → (𝐼‘𝐵) = 𝐵) |
| 31 | | ineq1 4213 |
. . . . . . . 8
⊢ ((𝐼‘𝐵) = 𝐵 → ((𝐼‘𝐵) ∩ (𝐼‘∅)) = (𝐵 ∩ (𝐼‘∅))) |
| 32 | | incom 4209 |
. . . . . . . 8
⊢ (𝐵 ∩ (𝐼‘∅)) = ((𝐼‘∅) ∩ 𝐵) |
| 33 | 31, 32 | eqtrdi 2793 |
. . . . . . 7
⊢ ((𝐼‘𝐵) = 𝐵 → ((𝐼‘𝐵) ∩ (𝐼‘∅)) = ((𝐼‘∅) ∩ 𝐵)) |
| 34 | 33 | eqeq1d 2739 |
. . . . . 6
⊢ ((𝐼‘𝐵) = 𝐵 → (((𝐼‘𝐵) ∩ (𝐼‘∅)) = ∅ ↔ ((𝐼‘∅) ∩ 𝐵) = ∅)) |
| 35 | 34 | biimpd 229 |
. . . . 5
⊢ ((𝐼‘𝐵) = 𝐵 → (((𝐼‘𝐵) ∩ (𝐼‘∅)) = ∅ → ((𝐼‘∅) ∩ 𝐵) = ∅)) |
| 36 | | reldisj 4453 |
. . . . . . 7
⊢ ((𝐼‘∅) ⊆ 𝐵 → (((𝐼‘∅) ∩ 𝐵) = ∅ ↔ (𝐼‘∅) ⊆ (𝐵 ∖ 𝐵))) |
| 37 | 36 | biimpd 229 |
. . . . . 6
⊢ ((𝐼‘∅) ⊆ 𝐵 → (((𝐼‘∅) ∩ 𝐵) = ∅ → (𝐼‘∅) ⊆ (𝐵 ∖ 𝐵))) |
| 38 | | difid 4376 |
. . . . . . . 8
⊢ (𝐵 ∖ 𝐵) = ∅ |
| 39 | 38 | sseq2i 4013 |
. . . . . . 7
⊢ ((𝐼‘∅) ⊆ (𝐵 ∖ 𝐵) ↔ (𝐼‘∅) ⊆
∅) |
| 40 | | ss0 4402 |
. . . . . . 7
⊢ ((𝐼‘∅) ⊆ ∅
→ (𝐼‘∅) =
∅) |
| 41 | 39, 40 | sylbi 217 |
. . . . . 6
⊢ ((𝐼‘∅) ⊆ (𝐵 ∖ 𝐵) → (𝐼‘∅) = ∅) |
| 42 | 37, 41 | syl6com 37 |
. . . . 5
⊢ (((𝐼‘∅) ∩ 𝐵) = ∅ → ((𝐼‘∅) ⊆ 𝐵 → (𝐼‘∅) = ∅)) |
| 43 | 35, 42 | syl6com 37 |
. . . 4
⊢ (((𝐼‘𝐵) ∩ (𝐼‘∅)) = ∅ → ((𝐼‘𝐵) = 𝐵 → ((𝐼‘∅) ⊆ 𝐵 → (𝐼‘∅) =
∅))) |
| 44 | 43 | com13 88 |
. . 3
⊢ ((𝐼‘∅) ⊆ 𝐵 → ((𝐼‘𝐵) = 𝐵 → (((𝐼‘𝐵) ∩ (𝐼‘∅)) = ∅ → (𝐼‘∅) =
∅))) |
| 45 | 29, 30, 44 | syl2im 40 |
. 2
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → (((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) → (((𝐼‘𝐵) ∩ (𝐼‘∅)) = ∅ → (𝐼‘∅) =
∅))) |
| 46 | 24, 45 | mpdd 43 |
1
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐼 ∈ (𝒫 𝐵 ↑m 𝒫 𝐵)) → (((𝐼‘𝐵) = 𝐵 ∧ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) → (𝐼‘∅) = ∅)) |