Proof of Theorem finnisoeu
| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . 5
⊢
OrdIso(𝑅, 𝐴) = OrdIso(𝑅, 𝐴) |
| 2 | 1 | oiexg 9575 |
. . . 4
⊢ (𝐴 ∈ Fin → OrdIso(𝑅, 𝐴) ∈ V) |
| 3 | 2 | adantl 481 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → OrdIso(𝑅, 𝐴) ∈ V) |
| 4 | | simpr 484 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ Fin) |
| 5 | | wofi 9325 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 We 𝐴) |
| 6 | 1 | oiiso 9577 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → OrdIso(𝑅, 𝐴) Isom E , 𝑅 (dom OrdIso(𝑅, 𝐴), 𝐴)) |
| 7 | 4, 5, 6 | syl2anc 584 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → OrdIso(𝑅, 𝐴) Isom E , 𝑅 (dom OrdIso(𝑅, 𝐴), 𝐴)) |
| 8 | 1 | oien 9578 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom OrdIso(𝑅, 𝐴) ≈ 𝐴) |
| 9 | 4, 5, 8 | syl2anc 584 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom OrdIso(𝑅, 𝐴) ≈ 𝐴) |
| 10 | | ficardid 10002 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ≈
𝐴) |
| 11 | 10 | adantl 481 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (card‘𝐴) ≈ 𝐴) |
| 12 | 11 | ensymd 9045 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ≈ (card‘𝐴)) |
| 13 | | entr 9046 |
. . . . . . 7
⊢ ((dom
OrdIso(𝑅, 𝐴) ≈ 𝐴 ∧ 𝐴 ≈ (card‘𝐴)) → dom OrdIso(𝑅, 𝐴) ≈ (card‘𝐴)) |
| 14 | 9, 12, 13 | syl2anc 584 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom OrdIso(𝑅, 𝐴) ≈ (card‘𝐴)) |
| 15 | 1 | oion 9576 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin → dom
OrdIso(𝑅, 𝐴) ∈ On) |
| 16 | 15 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom OrdIso(𝑅, 𝐴) ∈ On) |
| 17 | | ficardom 10001 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ∈
ω) |
| 18 | 17 | adantl 481 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (card‘𝐴) ∈
ω) |
| 19 | | onomeneq 9265 |
. . . . . . 7
⊢ ((dom
OrdIso(𝑅, 𝐴) ∈ On ∧ (card‘𝐴) ∈ ω) → (dom
OrdIso(𝑅, 𝐴) ≈ (card‘𝐴) ↔ dom OrdIso(𝑅, 𝐴) = (card‘𝐴))) |
| 20 | 16, 18, 19 | syl2anc 584 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (dom OrdIso(𝑅, 𝐴) ≈ (card‘𝐴) ↔ dom OrdIso(𝑅, 𝐴) = (card‘𝐴))) |
| 21 | 14, 20 | mpbid 232 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom OrdIso(𝑅, 𝐴) = (card‘𝐴)) |
| 22 | | isoeq4 7340 |
. . . . 5
⊢ (dom
OrdIso(𝑅, 𝐴) = (card‘𝐴) → (OrdIso(𝑅, 𝐴) Isom E , 𝑅 (dom OrdIso(𝑅, 𝐴), 𝐴) ↔ OrdIso(𝑅, 𝐴) Isom E , 𝑅 ((card‘𝐴), 𝐴))) |
| 23 | 21, 22 | syl 17 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (OrdIso(𝑅, 𝐴) Isom E , 𝑅 (dom OrdIso(𝑅, 𝐴), 𝐴) ↔ OrdIso(𝑅, 𝐴) Isom E , 𝑅 ((card‘𝐴), 𝐴))) |
| 24 | 7, 23 | mpbid 232 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → OrdIso(𝑅, 𝐴) Isom E , 𝑅 ((card‘𝐴), 𝐴)) |
| 25 | | isoeq1 7337 |
. . 3
⊢ (𝑓 = OrdIso(𝑅, 𝐴) → (𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴) ↔ OrdIso(𝑅, 𝐴) Isom E , 𝑅 ((card‘𝐴), 𝐴))) |
| 26 | 3, 24, 25 | spcedv 3598 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴)) |
| 27 | | wemoiso2 7999 |
. . 3
⊢ (𝑅 We 𝐴 → ∃*𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴)) |
| 28 | 5, 27 | syl 17 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃*𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴)) |
| 29 | | df-eu 2569 |
. 2
⊢
(∃!𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴) ↔ (∃𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴) ∧ ∃*𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴))) |
| 30 | 26, 28, 29 | sylanbrc 583 |
1
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃!𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴)) |