Step | Hyp | Ref
| Expression |
1 | | bren 8636 |
. 2
⊢ ((𝐴 × 𝐴) ≈ 𝐴 ↔ ∃𝑓 𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴) |
2 | | n0 4261 |
. 2
⊢ (𝐴 ≠ ∅ ↔
∃𝑏 𝑏 ∈ 𝐴) |
3 | | exdistrv 1964 |
. . 3
⊢
(∃𝑓∃𝑏(𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) ↔ (∃𝑓 𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ ∃𝑏 𝑏 ∈ 𝐴)) |
4 | | omex 9258 |
. . . . . . 7
⊢ ω
∈ V |
5 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴) |
6 | | f1ofo 6668 |
. . . . . . . . 9
⊢ (𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 → 𝑓:(𝐴 × 𝐴)–onto→𝐴) |
7 | | forn 6636 |
. . . . . . . . 9
⊢ (𝑓:(𝐴 × 𝐴)–onto→𝐴 → ran 𝑓 = 𝐴) |
8 | 5, 6, 7 | 3syl 18 |
. . . . . . . 8
⊢ ((𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → ran 𝑓 = 𝐴) |
9 | | vex 3412 |
. . . . . . . . 9
⊢ 𝑓 ∈ V |
10 | 9 | rnex 7690 |
. . . . . . . 8
⊢ ran 𝑓 ∈ V |
11 | 8, 10 | eqeltrrdi 2847 |
. . . . . . 7
⊢ ((𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → 𝐴 ∈ V) |
12 | | xpexg 7535 |
. . . . . . 7
⊢ ((ω
∈ V ∧ 𝐴 ∈ V)
→ (ω × 𝐴)
∈ V) |
13 | 4, 11, 12 | sylancr 590 |
. . . . . 6
⊢ ((𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → (ω × 𝐴) ∈ V) |
14 | | simpr 488 |
. . . . . . 7
⊢ ((𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → 𝑏 ∈ 𝐴) |
15 | | eqid 2737 |
. . . . . . 7
⊢
seqω((𝑘 ∈ V, 𝑔 ∈ V ↦ (𝑦 ∈ (𝐴 ↑m suc 𝑘) ↦ ((𝑔‘(𝑦 ↾ 𝑘))𝑓(𝑦‘𝑘)))), {〈∅, 𝑏〉}) = seqω((𝑘 ∈ V, 𝑔 ∈ V ↦ (𝑦 ∈ (𝐴 ↑m suc 𝑘) ↦ ((𝑔‘(𝑦 ↾ 𝑘))𝑓(𝑦‘𝑘)))), {〈∅, 𝑏〉}) |
16 | | eqid 2737 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ↦ 〈dom 𝑥, ((seqω((𝑘 ∈ V, 𝑔 ∈ V ↦ (𝑦 ∈ (𝐴 ↑m suc 𝑘) ↦ ((𝑔‘(𝑦 ↾ 𝑘))𝑓(𝑦‘𝑘)))), {〈∅, 𝑏〉})‘dom 𝑥)‘𝑥)〉) = (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) ↦ 〈dom 𝑥, ((seqω((𝑘 ∈ V, 𝑔 ∈ V ↦ (𝑦 ∈ (𝐴 ↑m suc 𝑘) ↦ ((𝑔‘(𝑦 ↾ 𝑘))𝑓(𝑦‘𝑘)))), {〈∅, 𝑏〉})‘dom 𝑥)‘𝑥)〉) |
17 | 11, 14, 5, 15, 16 | fseqenlem2 9639 |
. . . . . 6
⊢ ((𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) ↦ 〈dom 𝑥, ((seqω((𝑘 ∈ V, 𝑔 ∈ V ↦ (𝑦 ∈ (𝐴 ↑m suc 𝑘) ↦ ((𝑔‘(𝑦 ↾ 𝑘))𝑓(𝑦‘𝑘)))), {〈∅, 𝑏〉})‘dom 𝑥)‘𝑥)〉):∪
𝑛 ∈ ω (𝐴 ↑m 𝑛)–1-1→(ω × 𝐴)) |
18 | | f1domg 8648 |
. . . . . 6
⊢ ((ω
× 𝐴) ∈ V →
((𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ↦ 〈dom 𝑥, ((seqω((𝑘 ∈ V, 𝑔 ∈ V ↦ (𝑦 ∈ (𝐴 ↑m suc 𝑘) ↦ ((𝑔‘(𝑦 ↾ 𝑘))𝑓(𝑦‘𝑘)))), {〈∅, 𝑏〉})‘dom 𝑥)‘𝑥)〉):∪
𝑛 ∈ ω (𝐴 ↑m 𝑛)–1-1→(ω × 𝐴) → ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) ≼ (ω × 𝐴))) |
19 | 13, 17, 18 | sylc 65 |
. . . . 5
⊢ ((𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) ≼ (ω × 𝐴)) |
20 | | fseqdom 9640 |
. . . . . 6
⊢ (𝐴 ∈ V → (ω
× 𝐴) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
21 | 11, 20 | syl 17 |
. . . . 5
⊢ ((𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → (ω × 𝐴) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) |
22 | | sbth 8766 |
. . . . 5
⊢
((∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ≼ (ω × 𝐴) ∧ (ω × 𝐴) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛)) → ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) ≈ (ω × 𝐴)) |
23 | 19, 21, 22 | syl2anc 587 |
. . . 4
⊢ ((𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) ≈ (ω × 𝐴)) |
24 | 23 | exlimivv 1940 |
. . 3
⊢
(∃𝑓∃𝑏(𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ 𝑏 ∈ 𝐴) → ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) ≈ (ω × 𝐴)) |
25 | 3, 24 | sylbir 238 |
. 2
⊢
((∃𝑓 𝑓:(𝐴 × 𝐴)–1-1-onto→𝐴 ∧ ∃𝑏 𝑏 ∈ 𝐴) → ∪
𝑛 ∈ ω (𝐴 ↑m 𝑛) ≈ (ω × 𝐴)) |
26 | 1, 2, 25 | syl2anb 601 |
1
⊢ (((𝐴 × 𝐴) ≈ 𝐴 ∧ 𝐴 ≠ ∅) → ∪ 𝑛 ∈ ω (𝐴 ↑m 𝑛) ≈ (ω × 𝐴)) |