Step | Hyp | Ref
| Expression |
1 | | infxpenc2.2 |
. . . 4
⊢ (𝜑 → ∀𝑏 ∈ 𝐴 (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
2 | 1 | r19.21bi 2916 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐴) → (ω ⊆ 𝑏 → ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
3 | 2 | impr 647 |
. 2
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → ∃𝑤 ∈ (On ∖
1𝑜)(𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)) |
4 | | simpr 476 |
. . 3
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
5 | | infxpenc2.3 |
. . . . . 6
⊢ 𝑊 = (◡(𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘ran (𝑛‘𝑏)) |
6 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑤 → (ω ↑𝑜
𝑥) = (ω
↑𝑜 𝑤)) |
7 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (On ∖
1𝑜) ↦ (ω ↑𝑜 𝑥)) = (𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥)) |
8 | | ovex 6577 |
. . . . . . . . . 10
⊢ (ω
↑𝑜 𝑤) ∈ V |
9 | 6, 7, 8 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑤 ∈ (On ∖
1𝑜) → ((𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘𝑤) = (ω ↑𝑜 𝑤)) |
10 | 9 | ad2antrl 760 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → ((𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘𝑤) = (ω ↑𝑜 𝑤)) |
11 | | f1ofo 6057 |
. . . . . . . . . 10
⊢ ((𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤) → (𝑛‘𝑏):𝑏–onto→(ω ↑𝑜 𝑤)) |
12 | 11 | ad2antll 761 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (𝑛‘𝑏):𝑏–onto→(ω ↑𝑜 𝑤)) |
13 | | forn 6031 |
. . . . . . . . 9
⊢ ((𝑛‘𝑏):𝑏–onto→(ω ↑𝑜 𝑤) → ran (𝑛‘𝑏) = (ω ↑𝑜 𝑤)) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → ran (𝑛‘𝑏) = (ω ↑𝑜 𝑤)) |
15 | 10, 14 | eqtr4d 2647 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → ((𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘𝑤) = ran (𝑛‘𝑏)) |
16 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (ω
↑𝑜 𝑥) ∈ V |
17 | 16 | 2a1i 12 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (𝑥 ∈ (On ∖ 1𝑜)
→ (ω ↑𝑜 𝑥) ∈ V)) |
18 | | omelon 8426 |
. . . . . . . . . . . . . 14
⊢ ω
∈ On |
19 | | 1onn 7606 |
. . . . . . . . . . . . . 14
⊢
1𝑜 ∈ ω |
20 | | ondif2 7469 |
. . . . . . . . . . . . . 14
⊢ (ω
∈ (On ∖ 2𝑜) ↔ (ω ∈ On ∧
1𝑜 ∈ ω)) |
21 | 18, 19, 20 | mpbir2an 957 |
. . . . . . . . . . . . 13
⊢ ω
∈ (On ∖ 2𝑜) |
22 | 21 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) ∧ (𝑥 ∈ (On ∖ 1𝑜)
∧ 𝑦 ∈ (On ∖
1𝑜))) → ω ∈ (On ∖
2𝑜)) |
23 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (On ∖
1𝑜) → 𝑥 ∈ On) |
24 | 23 | ad2antrl 760 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) ∧ (𝑥 ∈ (On ∖ 1𝑜)
∧ 𝑦 ∈ (On ∖
1𝑜))) → 𝑥 ∈ On) |
25 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (On ∖
1𝑜) → 𝑦 ∈ On) |
26 | 25 | ad2antll 761 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) ∧ (𝑥 ∈ (On ∖ 1𝑜)
∧ 𝑦 ∈ (On ∖
1𝑜))) → 𝑦 ∈ On) |
27 | | oecan 7556 |
. . . . . . . . . . . 12
⊢ ((ω
∈ (On ∖ 2𝑜) ∧ 𝑥 ∈ On ∧ 𝑦 ∈ On) → ((ω
↑𝑜 𝑥) = (ω ↑𝑜 𝑦) ↔ 𝑥 = 𝑦)) |
28 | 22, 24, 26, 27 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) ∧ (𝑥 ∈ (On ∖ 1𝑜)
∧ 𝑦 ∈ (On ∖
1𝑜))) → ((ω ↑𝑜 𝑥) = (ω
↑𝑜 𝑦) ↔ 𝑥 = 𝑦)) |
29 | 28 | ex 449 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → ((𝑥 ∈ (On ∖ 1𝑜)
∧ 𝑦 ∈ (On ∖
1𝑜)) → ((ω ↑𝑜 𝑥) = (ω
↑𝑜 𝑦) ↔ 𝑥 = 𝑦))) |
30 | 17, 29 | dom2lem 7881 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥)):(On ∖
1𝑜)–1-1→V) |
31 | | f1f1orn 6061 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (On ∖
1𝑜) ↦ (ω ↑𝑜 𝑥)):(On ∖
1𝑜)–1-1→V
→ (𝑥 ∈ (On
∖ 1𝑜) ↦ (ω ↑𝑜
𝑥)):(On ∖
1𝑜)–1-1-onto→ran (𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))) |
32 | 30, 31 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥)):(On ∖
1𝑜)–1-1-onto→ran (𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))) |
33 | | simprl 790 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → 𝑤 ∈ (On ∖
1𝑜)) |
34 | | f1ocnvfv 6434 |
. . . . . . . 8
⊢ (((𝑥 ∈ (On ∖
1𝑜) ↦ (ω ↑𝑜 𝑥)):(On ∖
1𝑜)–1-1-onto→ran (𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥)) ∧ 𝑤 ∈ (On ∖ 1𝑜))
→ (((𝑥 ∈ (On
∖ 1𝑜) ↦ (ω ↑𝑜
𝑥))‘𝑤) = ran (𝑛‘𝑏) → (◡(𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘ran (𝑛‘𝑏)) = 𝑤)) |
35 | 32, 33, 34 | syl2anc 691 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (((𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘𝑤) = ran (𝑛‘𝑏) → (◡(𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘ran (𝑛‘𝑏)) = 𝑤)) |
36 | 15, 35 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (◡(𝑥 ∈ (On ∖ 1𝑜)
↦ (ω ↑𝑜 𝑥))‘ran (𝑛‘𝑏)) = 𝑤) |
37 | 5, 36 | syl5eq 2656 |
. . . . 5
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → 𝑊 = 𝑤) |
38 | 37 | eleq1d 2672 |
. . . 4
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (𝑊 ∈ (On ∖ 1𝑜)
↔ 𝑤 ∈ (On ∖
1𝑜))) |
39 | 37 | oveq2d 6565 |
. . . . 5
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (ω
↑𝑜 𝑊) = (ω ↑𝑜
𝑤)) |
40 | | f1oeq3 6042 |
. . . . 5
⊢ ((ω
↑𝑜 𝑊) = (ω ↑𝑜
𝑤) → ((𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊) ↔ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
41 | 39, 40 | syl 17 |
. . . 4
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → ((𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊) ↔ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) |
42 | 38, 41 | anbi12d 743 |
. . 3
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → ((𝑊 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊)) ↔ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤)))) |
43 | 4, 42 | mpbird 246 |
. 2
⊢ (((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) ∧ (𝑤 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑤))) → (𝑊 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊))) |
44 | 3, 43 | rexlimddv 3017 |
1
⊢ ((𝜑 ∧ (𝑏 ∈ 𝐴 ∧ ω ⊆ 𝑏)) → (𝑊 ∈ (On ∖ 1𝑜)
∧ (𝑛‘𝑏):𝑏–1-1-onto→(ω ↑𝑜 𝑊))) |