Proof of Theorem ntrneikb
Step | Hyp | Ref
| Expression |
1 | | con34b 306 |
. . . . . . 7
⊢ (((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ (¬ (𝑠 ∩ 𝑡) ≠ ∅ → ¬ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)))) |
2 | 1 | albii 1747 |
. . . . . 6
⊢
(∀𝑥((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ∀𝑥(¬ (𝑠 ∩ 𝑡) ≠ ∅ → ¬ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)))) |
3 | | 19.21v 1868 |
. . . . . 6
⊢
(∀𝑥(¬
(𝑠 ∩ 𝑡) ≠ ∅ → ¬ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡))) ↔ (¬ (𝑠 ∩ 𝑡) ≠ ∅ → ∀𝑥 ¬ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)))) |
4 | | nne 2798 |
. . . . . . 7
⊢ (¬
(𝑠 ∩ 𝑡) ≠ ∅ ↔ (𝑠 ∩ 𝑡) = ∅) |
5 | | elin 3796 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ↔ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡))) |
6 | 5 | imbi1i 339 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) → 𝑥 ∈ ∅) ↔ ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → 𝑥 ∈ ∅)) |
7 | | noel 3919 |
. . . . . . . . . . 11
⊢ ¬
𝑥 ∈
∅ |
8 | | imnot 355 |
. . . . . . . . . . 11
⊢ (¬
𝑥 ∈ ∅ →
(((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → 𝑥 ∈ ∅) ↔ ¬ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → 𝑥 ∈ ∅) ↔ ¬ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡))) |
10 | 6, 9 | bitr2i 265 |
. . . . . . . . 9
⊢ (¬
(𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) ↔ (𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) → 𝑥 ∈ ∅)) |
11 | 10 | albii 1747 |
. . . . . . . 8
⊢
(∀𝑥 ¬
(𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) ↔ ∀𝑥(𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) → 𝑥 ∈ ∅)) |
12 | | dfss2 3591 |
. . . . . . . 8
⊢ (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ ∅ ↔ ∀𝑥(𝑥 ∈ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) → 𝑥 ∈ ∅)) |
13 | | ss0b 3973 |
. . . . . . . 8
⊢ (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ ∅ ↔ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) |
14 | 11, 12, 13 | 3bitr2i 288 |
. . . . . . 7
⊢
(∀𝑥 ¬
(𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) ↔ ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) |
15 | 4, 14 | imbi12i 340 |
. . . . . 6
⊢ ((¬
(𝑠 ∩ 𝑡) ≠ ∅ → ∀𝑥 ¬ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡))) ↔ ((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅)) |
16 | 2, 3, 15 | 3bitrri 287 |
. . . . 5
⊢ (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑥((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅)) |
17 | | ntrnei.o |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑂 = (𝑖 ∈ V, 𝑗 ∈ V ↦ (𝑘 ∈ (𝒫 𝑗 ↑𝑚 𝑖) ↦ (𝑙 ∈ 𝑗 ↦ {𝑚 ∈ 𝑖 ∣ 𝑙 ∈ (𝑘‘𝑚)}))) |
18 | | ntrnei.f |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐹 = (𝒫 𝐵𝑂𝐵) |
19 | | ntrnei.r |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐼𝐹𝑁) |
20 | 17, 18, 19 | ntrneiiex 38374 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑𝑚 𝒫 𝐵)) |
21 | | elmapi 7879 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐼 ∈ (𝒫 𝐵 ↑𝑚
𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐼:𝒫 𝐵⟶𝒫 𝐵) |
23 | 22 | ffvelrnda 6359 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐼‘𝑠) ∈ 𝒫 𝐵) |
24 | 23 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘𝑠) ∈ 𝒫 𝐵) |
25 | 24 | elpwid 4170 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐼‘𝑠) ⊆ 𝐵) |
26 | 25 | sseld 3602 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝑥 ∈ (𝐼‘𝑠) → 𝑥 ∈ 𝐵)) |
27 | 26 | adantrd 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → 𝑥 ∈ 𝐵)) |
28 | 27 | imp 445 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡))) → 𝑥 ∈ 𝐵) |
29 | | biimt 350 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐵 → ((𝑠 ∩ 𝑡) ≠ ∅ ↔ (𝑥 ∈ 𝐵 → (𝑠 ∩ 𝑡) ≠ ∅))) |
30 | 28, 29 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ (𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡))) → ((𝑠 ∩ 𝑡) ≠ ∅ ↔ (𝑥 ∈ 𝐵 → (𝑠 ∩ 𝑡) ≠ ∅))) |
31 | 30 | pm5.74da 723 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑥 ∈ 𝐵 → (𝑠 ∩ 𝑡) ≠ ∅)))) |
32 | | bi2.04 376 |
. . . . . . . . 9
⊢ (((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑥 ∈ 𝐵 → (𝑠 ∩ 𝑡) ≠ ∅)) ↔ (𝑥 ∈ 𝐵 → ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
33 | 31, 32 | syl6bb 276 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ (𝑥 ∈ 𝐵 → ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅)))) |
34 | 33 | albidv 1849 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅)))) |
35 | | df-ral 2917 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐵 ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ∀𝑥(𝑥 ∈ 𝐵 → ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
36 | 34, 35 | syl6bbr 278 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ∀𝑥 ∈ 𝐵 ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
37 | 19 | ad3antrrr 766 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝐼𝐹𝑁) |
38 | | simpr 477 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐵) |
39 | | simpllr 799 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑠 ∈ 𝒫 𝐵) |
40 | 17, 18, 37, 38, 39 | ntrneiel 38379 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝐼‘𝑠) ↔ 𝑠 ∈ (𝑁‘𝑥))) |
41 | | simplr 792 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → 𝑡 ∈ 𝒫 𝐵) |
42 | 17, 18, 37, 38, 41 | ntrneiel 38379 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → (𝑥 ∈ (𝐼‘𝑡) ↔ 𝑡 ∈ (𝑁‘𝑥))) |
43 | 40, 42 | anbi12d 747 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)))) |
44 | 43 | imbi1d 331 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) ∧ 𝑥 ∈ 𝐵) → (((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
45 | 44 | ralbidva 2985 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥 ∈ 𝐵 ((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ∀𝑥 ∈ 𝐵 ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
46 | 36, 45 | bitrd 268 |
. . . . 5
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (∀𝑥((𝑥 ∈ (𝐼‘𝑠) ∧ 𝑥 ∈ (𝐼‘𝑡)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ∀𝑥 ∈ 𝐵 ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
47 | 16, 46 | syl5bb 272 |
. . . 4
⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) ∧ 𝑡 ∈ 𝒫 𝐵) → (((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑥 ∈ 𝐵 ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
48 | 47 | ralbidva 2985 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑡 ∈ 𝒫 𝐵∀𝑥 ∈ 𝐵 ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
49 | 48 | ralbidva 2985 |
. 2
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵∀𝑥 ∈ 𝐵 ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
50 | | alrot3 2038 |
. . . 4
⊢
(∀𝑥∀𝑠∀𝑡((𝑥 ∈ 𝐵 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)) ↔ ∀𝑠∀𝑡∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
51 | | 3anrot 1043 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) ↔ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑥 ∈ 𝐵)) |
52 | 51 | imbi1i 339 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐵 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)) ↔ ((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑥 ∈ 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
53 | 52 | albii 1747 |
. . . . 5
⊢
(∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)) ↔ ∀𝑥((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑥 ∈ 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
54 | 53 | 2albii 1748 |
. . . 4
⊢
(∀𝑠∀𝑡∀𝑥((𝑥 ∈ 𝐵 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)) ↔ ∀𝑠∀𝑡∀𝑥((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑥 ∈ 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
55 | 50, 54 | bitr2i 265 |
. . 3
⊢
(∀𝑠∀𝑡∀𝑥((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑥 ∈ 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)) ↔ ∀𝑥∀𝑠∀𝑡((𝑥 ∈ 𝐵 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
56 | | r3al 2940 |
. . 3
⊢
(∀𝑠 ∈
𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵∀𝑥 ∈ 𝐵 ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ∀𝑠∀𝑡∀𝑥((𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑥 ∈ 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
57 | | r3al 2940 |
. . 3
⊢
(∀𝑥 ∈
𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ∀𝑥∀𝑠∀𝑡((𝑥 ∈ 𝐵 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |
58 | 55, 56, 57 | 3bitr4i 292 |
. 2
⊢
(∀𝑠 ∈
𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵∀𝑥 ∈ 𝐵 ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅)) |
59 | 49, 58 | syl6bb 276 |
1
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∩ 𝑡) = ∅ → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ∅) ↔ ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑡 ∈ (𝑁‘𝑥)) → (𝑠 ∩ 𝑡) ≠ ∅))) |