| Step | Hyp | Ref
| Expression |
| 1 | | qtopbas 24780 |
. . . 4
⊢ ((,)
“ (ℚ × ℚ)) ∈ TopBases |
| 2 | | eltg3 22969 |
. . . 4
⊢ (((,)
“ (ℚ × ℚ)) ∈ TopBases → (𝐴 ∈ (topGen‘((,) “ (ℚ
× ℚ))) ↔ ∃𝑥(𝑥 ⊆ ((,) “ (ℚ ×
ℚ)) ∧ 𝐴 = ∪ 𝑥))) |
| 3 | 1, 2 | ax-mp 5 |
. . 3
⊢ (𝐴 ∈ (topGen‘((,)
“ (ℚ × ℚ))) ↔ ∃𝑥(𝑥 ⊆ ((,) “ (ℚ ×
ℚ)) ∧ 𝐴 = ∪ 𝑥)) |
| 4 | | uniiun 5058 |
. . . . . . 7
⊢ ∪ 𝑥 =
∪ 𝑦 ∈ 𝑥 𝑦 |
| 5 | | ssdomg 9040 |
. . . . . . . . . 10
⊢ (((,)
“ (ℚ × ℚ)) ∈ TopBases → (𝑥 ⊆ ((,) “ (ℚ ×
ℚ)) → 𝑥 ≼
((,) “ (ℚ × ℚ)))) |
| 6 | 1, 5 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ⊆ ((,) “ (ℚ
× ℚ)) → 𝑥
≼ ((,) “ (ℚ × ℚ))) |
| 7 | | omelon 9686 |
. . . . . . . . . . . 12
⊢ ω
∈ On |
| 8 | | qnnen 16249 |
. . . . . . . . . . . . . . 15
⊢ ℚ
≈ ℕ |
| 9 | | xpen 9180 |
. . . . . . . . . . . . . . 15
⊢ ((ℚ
≈ ℕ ∧ ℚ ≈ ℕ) → (ℚ × ℚ)
≈ (ℕ × ℕ)) |
| 10 | 8, 8, 9 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ (ℚ
× ℚ) ≈ (ℕ × ℕ) |
| 11 | | xpnnen 16247 |
. . . . . . . . . . . . . 14
⊢ (ℕ
× ℕ) ≈ ℕ |
| 12 | 10, 11 | entri 9048 |
. . . . . . . . . . . . 13
⊢ (ℚ
× ℚ) ≈ ℕ |
| 13 | | nnenom 14021 |
. . . . . . . . . . . . 13
⊢ ℕ
≈ ω |
| 14 | 12, 13 | entr2i 9049 |
. . . . . . . . . . . 12
⊢ ω
≈ (ℚ × ℚ) |
| 15 | | isnumi 9986 |
. . . . . . . . . . . 12
⊢ ((ω
∈ On ∧ ω ≈ (ℚ × ℚ)) → (ℚ
× ℚ) ∈ dom card) |
| 16 | 7, 14, 15 | mp2an 692 |
. . . . . . . . . . 11
⊢ (ℚ
× ℚ) ∈ dom card |
| 17 | | ioof 13487 |
. . . . . . . . . . . . 13
⊢
(,):(ℝ* × ℝ*)⟶𝒫
ℝ |
| 18 | | ffun 6739 |
. . . . . . . . . . . . 13
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → Fun (,)) |
| 19 | 17, 18 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ Fun
(,) |
| 20 | | qssre 13001 |
. . . . . . . . . . . . . . 15
⊢ ℚ
⊆ ℝ |
| 21 | | ressxr 11305 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℝ* |
| 22 | 20, 21 | sstri 3993 |
. . . . . . . . . . . . . 14
⊢ ℚ
⊆ ℝ* |
| 23 | | xpss12 5700 |
. . . . . . . . . . . . . 14
⊢ ((ℚ
⊆ ℝ* ∧ ℚ ⊆ ℝ*) →
(ℚ × ℚ) ⊆ (ℝ* ×
ℝ*)) |
| 24 | 22, 22, 23 | mp2an 692 |
. . . . . . . . . . . . 13
⊢ (ℚ
× ℚ) ⊆ (ℝ* ×
ℝ*) |
| 25 | 17 | fdmi 6747 |
. . . . . . . . . . . . 13
⊢ dom (,) =
(ℝ* × ℝ*) |
| 26 | 24, 25 | sseqtrri 4033 |
. . . . . . . . . . . 12
⊢ (ℚ
× ℚ) ⊆ dom (,) |
| 27 | | fores 6830 |
. . . . . . . . . . . 12
⊢ ((Fun (,)
∧ (ℚ × ℚ) ⊆ dom (,)) → ((,) ↾ (ℚ
× ℚ)):(ℚ × ℚ)–onto→((,) “ (ℚ ×
ℚ))) |
| 28 | 19, 26, 27 | mp2an 692 |
. . . . . . . . . . 11
⊢ ((,)
↾ (ℚ × ℚ)):(ℚ × ℚ)–onto→((,) “ (ℚ ×
ℚ)) |
| 29 | | fodomnum 10097 |
. . . . . . . . . . 11
⊢ ((ℚ
× ℚ) ∈ dom card → (((,) ↾ (ℚ ×
ℚ)):(ℚ × ℚ)–onto→((,) “ (ℚ × ℚ)) →
((,) “ (ℚ × ℚ)) ≼ (ℚ ×
ℚ))) |
| 30 | 16, 28, 29 | mp2 9 |
. . . . . . . . . 10
⊢ ((,)
“ (ℚ × ℚ)) ≼ (ℚ ×
ℚ) |
| 31 | | domentr 9053 |
. . . . . . . . . 10
⊢ ((((,)
“ (ℚ × ℚ)) ≼ (ℚ × ℚ) ∧
(ℚ × ℚ) ≈ ℕ) → ((,) “ (ℚ ×
ℚ)) ≼ ℕ) |
| 32 | 30, 12, 31 | mp2an 692 |
. . . . . . . . 9
⊢ ((,)
“ (ℚ × ℚ)) ≼ ℕ |
| 33 | | domtr 9047 |
. . . . . . . . 9
⊢ ((𝑥 ≼ ((,) “ (ℚ
× ℚ)) ∧ ((,) “ (ℚ × ℚ)) ≼
ℕ) → 𝑥 ≼
ℕ) |
| 34 | 6, 32, 33 | sylancl 586 |
. . . . . . . 8
⊢ (𝑥 ⊆ ((,) “ (ℚ
× ℚ)) → 𝑥
≼ ℕ) |
| 35 | | imassrn 6089 |
. . . . . . . . . . 11
⊢ ((,)
“ (ℚ × ℚ)) ⊆ ran (,) |
| 36 | | ffn 6736 |
. . . . . . . . . . . . . 14
⊢
((,):(ℝ* × ℝ*)⟶𝒫
ℝ → (,) Fn (ℝ* ×
ℝ*)) |
| 37 | 17, 36 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (,) Fn
(ℝ* × ℝ*) |
| 38 | | ioombl 25600 |
. . . . . . . . . . . . . 14
⊢ (𝑥(,)𝑦) ∈ dom vol |
| 39 | 38 | rgen2w 3066 |
. . . . . . . . . . . . 13
⊢
∀𝑥 ∈
ℝ* ∀𝑦 ∈ ℝ* (𝑥(,)𝑦) ∈ dom vol |
| 40 | | ffnov 7559 |
. . . . . . . . . . . . 13
⊢
((,):(ℝ* × ℝ*)⟶dom vol
↔ ((,) Fn (ℝ* × ℝ*) ∧
∀𝑥 ∈
ℝ* ∀𝑦 ∈ ℝ* (𝑥(,)𝑦) ∈ dom vol)) |
| 41 | 37, 39, 40 | mpbir2an 711 |
. . . . . . . . . . . 12
⊢
(,):(ℝ* × ℝ*)⟶dom
vol |
| 42 | | frn 6743 |
. . . . . . . . . . . 12
⊢
((,):(ℝ* × ℝ*)⟶dom vol
→ ran (,) ⊆ dom vol) |
| 43 | 41, 42 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ran (,)
⊆ dom vol |
| 44 | 35, 43 | sstri 3993 |
. . . . . . . . . 10
⊢ ((,)
“ (ℚ × ℚ)) ⊆ dom vol |
| 45 | | sstr 3992 |
. . . . . . . . . 10
⊢ ((𝑥 ⊆ ((,) “ (ℚ
× ℚ)) ∧ ((,) “ (ℚ × ℚ)) ⊆ dom
vol) → 𝑥 ⊆ dom
vol) |
| 46 | 44, 45 | mpan2 691 |
. . . . . . . . 9
⊢ (𝑥 ⊆ ((,) “ (ℚ
× ℚ)) → 𝑥
⊆ dom vol) |
| 47 | | dfss3 3972 |
. . . . . . . . 9
⊢ (𝑥 ⊆ dom vol ↔
∀𝑦 ∈ 𝑥 𝑦 ∈ dom vol) |
| 48 | 46, 47 | sylib 218 |
. . . . . . . 8
⊢ (𝑥 ⊆ ((,) “ (ℚ
× ℚ)) → ∀𝑦 ∈ 𝑥 𝑦 ∈ dom vol) |
| 49 | | iunmbl2 25592 |
. . . . . . . 8
⊢ ((𝑥 ≼ ℕ ∧
∀𝑦 ∈ 𝑥 𝑦 ∈ dom vol) → ∪ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol) |
| 50 | 34, 48, 49 | syl2anc 584 |
. . . . . . 7
⊢ (𝑥 ⊆ ((,) “ (ℚ
× ℚ)) → ∪ 𝑦 ∈ 𝑥 𝑦 ∈ dom vol) |
| 51 | 4, 50 | eqeltrid 2845 |
. . . . . 6
⊢ (𝑥 ⊆ ((,) “ (ℚ
× ℚ)) → ∪ 𝑥 ∈ dom vol) |
| 52 | | eleq1 2829 |
. . . . . 6
⊢ (𝐴 = ∪
𝑥 → (𝐴 ∈ dom vol ↔ ∪ 𝑥
∈ dom vol)) |
| 53 | 51, 52 | syl5ibrcom 247 |
. . . . 5
⊢ (𝑥 ⊆ ((,) “ (ℚ
× ℚ)) → (𝐴
= ∪ 𝑥 → 𝐴 ∈ dom vol)) |
| 54 | 53 | imp 406 |
. . . 4
⊢ ((𝑥 ⊆ ((,) “ (ℚ
× ℚ)) ∧ 𝐴 =
∪ 𝑥) → 𝐴 ∈ dom vol) |
| 55 | 54 | exlimiv 1930 |
. . 3
⊢
(∃𝑥(𝑥 ⊆ ((,) “ (ℚ
× ℚ)) ∧ 𝐴 =
∪ 𝑥) → 𝐴 ∈ dom vol) |
| 56 | 3, 55 | sylbi 217 |
. 2
⊢ (𝐴 ∈ (topGen‘((,)
“ (ℚ × ℚ))) → 𝐴 ∈ dom vol) |
| 57 | | eqid 2737 |
. . 3
⊢
(topGen‘((,) “ (ℚ × ℚ))) =
(topGen‘((,) “ (ℚ × ℚ))) |
| 58 | 57 | tgqioo 24821 |
. 2
⊢
(topGen‘ran (,)) = (topGen‘((,) “ (ℚ ×
ℚ))) |
| 59 | 56, 58 | eleq2s 2859 |
1
⊢ (𝐴 ∈ (topGen‘ran (,))
→ 𝐴 ∈ dom
vol) |