Metamath Proof Explorer

Theorem finnisoeu

Description: A finite totally ordered set has a unique order isomorphism to a finite ordinal. (Contributed by Stefan O'Rear, 16-Nov-2014) (Proof shortened by Mario Carneiro, 26-Jun-2015)

Ref Expression
Assertion finnisoeu ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃! 𝑓 𝑓 Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ OrdIso ( 𝑅 , 𝐴 ) = OrdIso ( 𝑅 , 𝐴 )
2 1 oiexg ⊢ ( 𝐴 ∈ Fin → OrdIso ( 𝑅 , 𝐴 ) ∈ V )
3 2 adantl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → OrdIso ( 𝑅 , 𝐴 ) ∈ V )
4 simpr ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐴 ∈ Fin )
5 wofi ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑅 We 𝐴 )
6 1 oiiso ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑅 We 𝐴 ) → OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) )
7 4 5 6 syl2anc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) )
8 1 oien ⊢ ( ( 𝐴 ∈ Fin ∧ 𝑅 We 𝐴 ) → dom OrdIso ( 𝑅 , 𝐴 ) ≈ 𝐴 )
9 4 5 8 syl2anc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom OrdIso ( 𝑅 , 𝐴 ) ≈ 𝐴 )
10 ficardid ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ≈ 𝐴 )
11 10 adantl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( card ‘ 𝐴 ) ≈ 𝐴 )
12 11 ensymd ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝐴 ≈ ( card ‘ 𝐴 ) )
13 entr ⊢ ( ( dom OrdIso ( 𝑅 , 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≈ ( card ‘ 𝐴 ) ) → dom OrdIso ( 𝑅 , 𝐴 ) ≈ ( card ‘ 𝐴 ) )
14 9 12 13 syl2anc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom OrdIso ( 𝑅 , 𝐴 ) ≈ ( card ‘ 𝐴 ) )
15 1 oion ⊢ ( 𝐴 ∈ Fin → dom OrdIso ( 𝑅 , 𝐴 ) ∈ On )
16 15 adantl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom OrdIso ( 𝑅 , 𝐴 ) ∈ On )
17 ficardom ⊢ ( 𝐴 ∈ Fin → ( card ‘ 𝐴 ) ∈ ω )
18 17 adantl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( card ‘ 𝐴 ) ∈ ω )
19 onomeneq ⊢ ( ( dom OrdIso ( 𝑅 , 𝐴 ) ∈ On ∧ ( card ‘ 𝐴 ) ∈ ω ) → ( dom OrdIso ( 𝑅 , 𝐴 ) ≈ ( card ‘ 𝐴 ) ↔ dom OrdIso ( 𝑅 , 𝐴 ) = ( card ‘ 𝐴 ) ) )
20 16 18 19 syl2anc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( dom OrdIso ( 𝑅 , 𝐴 ) ≈ ( card ‘ 𝐴 ) ↔ dom OrdIso ( 𝑅 , 𝐴 ) = ( card ‘ 𝐴 ) ) )
21 14 20 mpbid ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → dom OrdIso ( 𝑅 , 𝐴 ) = ( card ‘ 𝐴 ) )
22 isoeq4 ⊢ ( dom OrdIso ( 𝑅 , 𝐴 ) = ( card ‘ 𝐴 ) → ( OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) ↔ OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) ) )
23 21 22 syl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) ↔ OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) ) )
24 7 23 mpbid ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) )
25 isoeq1 ⊢ ( 𝑓 = OrdIso ( 𝑅 , 𝐴 ) → ( 𝑓 Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) ↔ OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) ) )
26 3 24 25 spcedv ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃ 𝑓 𝑓 Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) )
27 wemoiso2 ⊢ ( 𝑅 We 𝐴 → ∃* 𝑓 𝑓 Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) )
28 5 27 syl ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃* 𝑓 𝑓 Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) )
29 df-eu ⊢ ( ∃! 𝑓 𝑓 Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) ↔ ( ∃ 𝑓 𝑓 Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) ∧ ∃* 𝑓 𝑓 Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) ) )
30 26 28 29 sylanbrc ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ∃! 𝑓 𝑓 Isom E , 𝑅 ( ( card ‘ 𝐴 ) , 𝐴 ) )