| Step | Hyp | Ref
| Expression |
| 1 | | fin23lem22.b |
. 2
⊢ 𝐶 = (𝑖 ∈ ω ↦ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)) |
| 2 | | fin23lem23 10366 |
. . 3
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) →
∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) |
| 3 | | riotacl 7405 |
. . 3
⊢
(∃!𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖 → (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) ∈ 𝑆) |
| 4 | 2, 3 | syl 17 |
. 2
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑖 ∈ ω) →
(℩𝑗 ∈
𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) ∈ 𝑆) |
| 5 | | simpll 767 |
. . . 4
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑎 ∈ 𝑆) → 𝑆 ⊆ ω) |
| 6 | | simpr 484 |
. . . 4
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ 𝑆) |
| 7 | 5, 6 | sseldd 3984 |
. . 3
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑎 ∈ 𝑆) → 𝑎 ∈ ω) |
| 8 | | nnfi 9207 |
. . 3
⊢ (𝑎 ∈ ω → 𝑎 ∈ Fin) |
| 9 | | infi 9302 |
. . 3
⊢ (𝑎 ∈ Fin → (𝑎 ∩ 𝑆) ∈ Fin) |
| 10 | | ficardom 10001 |
. . 3
⊢ ((𝑎 ∩ 𝑆) ∈ Fin → (card‘(𝑎 ∩ 𝑆)) ∈ ω) |
| 11 | 7, 8, 9, 10 | 4syl 19 |
. 2
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ 𝑎 ∈ 𝑆) → (card‘(𝑎 ∩ 𝑆)) ∈ ω) |
| 12 | | cardnn 10003 |
. . . . . . 7
⊢ (𝑖 ∈ ω →
(card‘𝑖) = 𝑖) |
| 13 | 12 | eqcomd 2743 |
. . . . . 6
⊢ (𝑖 ∈ ω → 𝑖 = (card‘𝑖)) |
| 14 | 13 | eqeq1d 2739 |
. . . . 5
⊢ (𝑖 ∈ ω → (𝑖 = (card‘(𝑎 ∩ 𝑆)) ↔ (card‘𝑖) = (card‘(𝑎 ∩ 𝑆)))) |
| 15 | | eqcom 2744 |
. . . . 5
⊢
((card‘𝑖) =
(card‘(𝑎 ∩ 𝑆)) ↔ (card‘(𝑎 ∩ 𝑆)) = (card‘𝑖)) |
| 16 | 14, 15 | bitrdi 287 |
. . . 4
⊢ (𝑖 ∈ ω → (𝑖 = (card‘(𝑎 ∩ 𝑆)) ↔ (card‘(𝑎 ∩ 𝑆)) = (card‘𝑖))) |
| 17 | 16 | ad2antrl 728 |
. . 3
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → (𝑖 = (card‘(𝑎 ∩ 𝑆)) ↔ (card‘(𝑎 ∩ 𝑆)) = (card‘𝑖))) |
| 18 | | simpll 767 |
. . . . . . 7
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → 𝑆 ⊆ ω) |
| 19 | | simprr 773 |
. . . . . . 7
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → 𝑎 ∈ 𝑆) |
| 20 | 18, 19 | sseldd 3984 |
. . . . . 6
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → 𝑎 ∈ ω) |
| 21 | | nnon 7893 |
. . . . . 6
⊢ (𝑎 ∈ ω → 𝑎 ∈ On) |
| 22 | | onenon 9989 |
. . . . . 6
⊢ (𝑎 ∈ On → 𝑎 ∈ dom
card) |
| 23 | 20, 21, 22 | 3syl 18 |
. . . . 5
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → 𝑎 ∈ dom card) |
| 24 | | inss1 4237 |
. . . . 5
⊢ (𝑎 ∩ 𝑆) ⊆ 𝑎 |
| 25 | | ssnum 10079 |
. . . . 5
⊢ ((𝑎 ∈ dom card ∧ (𝑎 ∩ 𝑆) ⊆ 𝑎) → (𝑎 ∩ 𝑆) ∈ dom card) |
| 26 | 23, 24, 25 | sylancl 586 |
. . . 4
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → (𝑎 ∩ 𝑆) ∈ dom card) |
| 27 | | nnon 7893 |
. . . . . 6
⊢ (𝑖 ∈ ω → 𝑖 ∈ On) |
| 28 | 27 | ad2antrl 728 |
. . . . 5
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → 𝑖 ∈ On) |
| 29 | | onenon 9989 |
. . . . 5
⊢ (𝑖 ∈ On → 𝑖 ∈ dom
card) |
| 30 | 28, 29 | syl 17 |
. . . 4
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → 𝑖 ∈ dom card) |
| 31 | | carden2 10027 |
. . . 4
⊢ (((𝑎 ∩ 𝑆) ∈ dom card ∧ 𝑖 ∈ dom card) → ((card‘(𝑎 ∩ 𝑆)) = (card‘𝑖) ↔ (𝑎 ∩ 𝑆) ≈ 𝑖)) |
| 32 | 26, 30, 31 | syl2anc 584 |
. . 3
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → ((card‘(𝑎 ∩ 𝑆)) = (card‘𝑖) ↔ (𝑎 ∩ 𝑆) ≈ 𝑖)) |
| 33 | 2 | adantrr 717 |
. . . . 5
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) |
| 34 | | ineq1 4213 |
. . . . . . 7
⊢ (𝑗 = 𝑎 → (𝑗 ∩ 𝑆) = (𝑎 ∩ 𝑆)) |
| 35 | 34 | breq1d 5153 |
. . . . . 6
⊢ (𝑗 = 𝑎 → ((𝑗 ∩ 𝑆) ≈ 𝑖 ↔ (𝑎 ∩ 𝑆) ≈ 𝑖)) |
| 36 | 35 | riota2 7413 |
. . . . 5
⊢ ((𝑎 ∈ 𝑆 ∧ ∃!𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) → ((𝑎 ∩ 𝑆) ≈ 𝑖 ↔ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = 𝑎)) |
| 37 | 19, 33, 36 | syl2anc 584 |
. . . 4
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → ((𝑎 ∩ 𝑆) ≈ 𝑖 ↔ (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = 𝑎)) |
| 38 | | eqcom 2744 |
. . . 4
⊢
((℩𝑗
∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖) = 𝑎 ↔ 𝑎 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖)) |
| 39 | 37, 38 | bitrdi 287 |
. . 3
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → ((𝑎 ∩ 𝑆) ≈ 𝑖 ↔ 𝑎 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))) |
| 40 | 17, 32, 39 | 3bitrd 305 |
. 2
⊢ (((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) ∧ (𝑖 ∈ ω ∧ 𝑎 ∈ 𝑆)) → (𝑖 = (card‘(𝑎 ∩ 𝑆)) ↔ 𝑎 = (℩𝑗 ∈ 𝑆 (𝑗 ∩ 𝑆) ≈ 𝑖))) |
| 41 | 1, 4, 11, 40 | f1o2d 7687 |
1
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝐶:ω–1-1-onto→𝑆) |