Step | Hyp | Ref
| Expression |
1 | | an4 656 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽) ∧ (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦)) ↔ ((𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥) ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦))) |
2 | | nnuz 12365 |
. . . . . . . . . . . . 13
⊢ ℕ =
(ℤ≥‘1) |
3 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → 𝐴 ∈ 𝑥) |
4 | | 1zzd 12096 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → 1 ∈ ℤ) |
5 | | lmmo.4 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐴) |
6 | 5 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → 𝐹(⇝𝑡‘𝐽)𝐴) |
7 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → 𝑥 ∈ 𝐽) |
8 | 2, 3, 4, 6, 7 | lmcvg 22015 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥) |
9 | 8 | ex 416 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥)) |
10 | | simprr 773 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → 𝐵 ∈ 𝑦) |
11 | | 1zzd 12096 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → 1 ∈ ℤ) |
12 | | lmmo.5 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝐵) |
13 | 12 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → 𝐹(⇝𝑡‘𝐽)𝐵) |
14 | | simprl 771 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → 𝑦 ∈ 𝐽) |
15 | 2, 10, 11, 13, 14 | lmcvg 22015 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦) |
16 | 15 | ex 416 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦) → ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦)) |
17 | 9, 16 | anim12d 612 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥) ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦))) |
18 | 2 | rexanuz2 14801 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦) ↔ (∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦)) |
19 | | nnz 12087 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℕ → 𝑗 ∈
ℤ) |
20 | | uzid 12341 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ ℤ → 𝑗 ∈
(ℤ≥‘𝑗)) |
21 | | ne0i 4223 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈
(ℤ≥‘𝑗) → (ℤ≥‘𝑗) ≠ ∅) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ ℕ →
(ℤ≥‘𝑗) ≠ ∅) |
23 | | r19.2z 4381 |
. . . . . . . . . . . . . 14
⊢
(((ℤ≥‘𝑗) ≠ ∅ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) → ∃𝑘 ∈ (ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) |
24 | | elin 3859 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘) ∈ (𝑥 ∩ 𝑦) ↔ ((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) |
25 | | n0i 4222 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐹‘𝑘) ∈ (𝑥 ∩ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
26 | 24, 25 | sylbir 238 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
27 | 26 | rexlimivw 3192 |
. . . . . . . . . . . . . 14
⊢
(∃𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
28 | 23, 27 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((ℤ≥‘𝑗) ≠ ∅ ∧ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) → ¬ (𝑥 ∩ 𝑦) = ∅) |
29 | 22, 28 | sylan 583 |
. . . . . . . . . . . 12
⊢ ((𝑗 ∈ ℕ ∧
∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦)) → ¬ (𝑥 ∩ 𝑦) = ∅) |
30 | 29 | rexlimiva 3191 |
. . . . . . . . . . 11
⊢
(∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)((𝐹‘𝑘) ∈ 𝑥 ∧ (𝐹‘𝑘) ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
31 | 18, 30 | sylbir 238 |
. . . . . . . . . 10
⊢
((∃𝑗 ∈
ℕ ∀𝑘 ∈
(ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑥 ∧ ∃𝑗 ∈ ℕ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐹‘𝑘) ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) |
32 | 17, 31 | syl6 35 |
. . . . . . . . 9
⊢ (𝜑 → (((𝑥 ∈ 𝐽 ∧ 𝐴 ∈ 𝑥) ∧ (𝑦 ∈ 𝐽 ∧ 𝐵 ∈ 𝑦)) → ¬ (𝑥 ∩ 𝑦) = ∅)) |
33 | 1, 32 | syl5bi 245 |
. . . . . . . 8
⊢ (𝜑 → (((𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽) ∧ (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦)) → ¬ (𝑥 ∩ 𝑦) = ∅)) |
34 | 33 | expdimp 456 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅)) |
35 | | imnan 403 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) → ¬ (𝑥 ∩ 𝑦) = ∅) ↔ ¬ ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) ∧ (𝑥 ∩ 𝑦) = ∅)) |
36 | 34, 35 | sylib 221 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ¬ ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) ∧ (𝑥 ∩ 𝑦) = ∅)) |
37 | | df-3an 1090 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅) ↔ ((𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦) ∧ (𝑥 ∩ 𝑦) = ∅)) |
38 | 36, 37 | sylnibr 332 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐽)) → ¬ (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
39 | 38 | anassrs 471 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐽) ∧ 𝑦 ∈ 𝐽) → ¬ (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
40 | 39 | nrexdv 3180 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → ¬ ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
41 | 40 | nrexdv 3180 |
. 2
⊢ (𝜑 → ¬ ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
42 | | lmmo.1 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ Haus) |
43 | | haustop 22084 |
. . . . . . 7
⊢ (𝐽 ∈ Haus → 𝐽 ∈ Top) |
44 | 42, 43 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ Top) |
45 | | toptopon2 21671 |
. . . . . 6
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) |
46 | 44, 45 | sylib 221 |
. . . . 5
⊢ (𝜑 → 𝐽 ∈ (TopOn‘∪ 𝐽)) |
47 | | lmcl 22050 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐹(⇝𝑡‘𝐽)𝐴) → 𝐴 ∈ ∪ 𝐽) |
48 | 46, 5, 47 | syl2anc 587 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ∪ 𝐽) |
49 | | lmcl 22050 |
. . . . 5
⊢ ((𝐽 ∈ (TopOn‘∪ 𝐽)
∧ 𝐹(⇝𝑡‘𝐽)𝐵) → 𝐵 ∈ ∪ 𝐽) |
50 | 46, 12, 49 | syl2anc 587 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ ∪ 𝐽) |
51 | | eqid 2738 |
. . . . . 6
⊢ ∪ 𝐽 =
∪ 𝐽 |
52 | 51 | hausnei 22081 |
. . . . 5
⊢ ((𝐽 ∈ Haus ∧ (𝐴 ∈ ∪ 𝐽
∧ 𝐵 ∈ ∪ 𝐽
∧ 𝐴 ≠ 𝐵)) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅)) |
53 | 52 | 3exp2 1355 |
. . . 4
⊢ (𝐽 ∈ Haus → (𝐴 ∈ ∪ 𝐽
→ (𝐵 ∈ ∪ 𝐽
→ (𝐴 ≠ 𝐵 → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))))) |
54 | 42, 48, 50, 53 | syl3c 66 |
. . 3
⊢ (𝜑 → (𝐴 ≠ 𝐵 → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅))) |
55 | 54 | necon1bd 2952 |
. 2
⊢ (𝜑 → (¬ ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐽 (𝐴 ∈ 𝑥 ∧ 𝐵 ∈ 𝑦 ∧ (𝑥 ∩ 𝑦) = ∅) → 𝐴 = 𝐵)) |
56 | 41, 55 | mpd 15 |
1
⊢ (𝜑 → 𝐴 = 𝐵) |