Proof of Theorem finnisoeu
Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . . 5
⊢
OrdIso(𝑅, 𝐴) = OrdIso(𝑅, 𝐴) |
2 | 1 | oiexg 8440 |
. . . 4
⊢ (𝐴 ∈ Fin → OrdIso(𝑅, 𝐴) ∈ V) |
3 | 2 | adantl 482 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → OrdIso(𝑅, 𝐴) ∈ V) |
4 | | simpr 477 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ∈ Fin) |
5 | | wofi 8209 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 We 𝐴) |
6 | 1 | oiiso 8442 |
. . . . 5
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → OrdIso(𝑅, 𝐴) Isom E , 𝑅 (dom OrdIso(𝑅, 𝐴), 𝐴)) |
7 | 4, 5, 6 | syl2anc 693 |
. . . 4
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → OrdIso(𝑅, 𝐴) Isom E , 𝑅 (dom OrdIso(𝑅, 𝐴), 𝐴)) |
8 | 1 | oien 8443 |
. . . . . . . 8
⊢ ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom OrdIso(𝑅, 𝐴) ≈ 𝐴) |
9 | 4, 5, 8 | syl2anc 693 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom OrdIso(𝑅, 𝐴) ≈ 𝐴) |
10 | | ficardid 8788 |
. . . . . . . . 9
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ≈
𝐴) |
11 | 10 | adantl 482 |
. . . . . . . 8
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (card‘𝐴) ≈ 𝐴) |
12 | 11 | ensymd 8007 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → 𝐴 ≈ (card‘𝐴)) |
13 | | entr 8008 |
. . . . . . 7
⊢ ((dom
OrdIso(𝑅, 𝐴) ≈ 𝐴 ∧ 𝐴 ≈ (card‘𝐴)) → dom OrdIso(𝑅, 𝐴) ≈ (card‘𝐴)) |
14 | 9, 12, 13 | syl2anc 693 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom OrdIso(𝑅, 𝐴) ≈ (card‘𝐴)) |
15 | 1 | oion 8441 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin → dom
OrdIso(𝑅, 𝐴) ∈ On) |
16 | 15 | adantl 482 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom OrdIso(𝑅, 𝐴) ∈ On) |
17 | | ficardom 8787 |
. . . . . . . 8
⊢ (𝐴 ∈ Fin →
(card‘𝐴) ∈
ω) |
18 | 17 | adantl 482 |
. . . . . . 7
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (card‘𝐴) ∈
ω) |
19 | | onomeneq 8150 |
. . . . . . 7
⊢ ((dom
OrdIso(𝑅, 𝐴) ∈ On ∧ (card‘𝐴) ∈ ω) → (dom
OrdIso(𝑅, 𝐴) ≈ (card‘𝐴) ↔ dom OrdIso(𝑅, 𝐴) = (card‘𝐴))) |
20 | 16, 18, 19 | syl2anc 693 |
. . . . . 6
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → (dom OrdIso(𝑅, 𝐴) ≈ (card‘𝐴) ↔ dom OrdIso(𝑅, 𝐴) = (card‘𝐴))) |
21 | 14, 20 | mpbid 222 |
. . . . 5
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → dom OrdIso(𝑅, 𝐴) = (card‘𝐴)) |
22 | | isoeq4 6570 |
. . . . 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 222 |
. . 3
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → OrdIso(𝑅, 𝐴) Isom E , 𝑅 ((card‘𝐴), 𝐴)) |
25 | | isoeq1 6567 |
. . . 4
⊢ (𝑓 = OrdIso(𝑅, 𝐴) → (𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴) ↔ OrdIso(𝑅, 𝐴) Isom E , 𝑅 ((card‘𝐴), 𝐴))) |
26 | 25 | spcegv 3294 |
. . 3
⊢
(OrdIso(𝑅, 𝐴) ∈ V → (OrdIso(𝑅, 𝐴) Isom E , 𝑅 ((card‘𝐴), 𝐴) → ∃𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴))) |
27 | 3, 24, 26 | sylc 65 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴)) |
28 | | wemoiso2 7154 |
. . 3
⊢ (𝑅 We 𝐴 → ∃*𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴)) |
29 | 5, 28 | syl 17 |
. 2
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃*𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴)) |
30 | | eu5 2496 |
. 2
⊢
(∃!𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴) ↔ (∃𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴) ∧ ∃*𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴))) |
31 | 27, 29, 30 | sylanbrc 698 |
1
⊢ ((𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin) → ∃!𝑓 𝑓 Isom E , 𝑅 ((card‘𝐴), 𝐴)) |