Metamath Proof Explorer

Theorem smoiso2

Description: The strictly monotone ordinal functions are also isomorphisms of subclasses of On equipped with the membership relation. (Contributed by Mario Carneiro, 20-Mar-2013)

Ref Expression
Assertion smoiso2 ( ( Ord 𝐴 ∧ 𝐵 ⊆ On ) → ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) ↔ 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 fof ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 : 𝐴 ⟶ 𝐵 )
2 smo11 ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ Smo 𝐹 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
3 1 2 sylan ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
4 simpl ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) → 𝐹 : 𝐴 –onto→ 𝐵 )
5 df-f1o ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ↔ ( 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝐹 : 𝐴 –onto→ 𝐵 ) )
6 3 4 5 sylanbrc ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
7 6 adantl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ On ) ∧ ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
8 fofn ⊢ ( 𝐹 : 𝐴 –onto→ 𝐵 → 𝐹 Fn 𝐴 )
9 smoord ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 ∈ 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
10 epel ⊢ ( 𝑥 E 𝑦 ↔ 𝑥 ∈ 𝑦 )
11 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
12 11 epeli ⊢ ( ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) )
13 9 10 12 3bitr4g ⊢ ( ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 E 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) ) )
14 13 ralrimivva ⊢ ( ( 𝐹 Fn 𝐴 ∧ Smo 𝐹 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 E 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) ) )
15 8 14 sylan ⊢ ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 E 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) ) )
16 15 adantl ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ On ) ∧ ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 E 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) ) )
17 df-isom ⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ↔ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 E 𝑦 ↔ ( 𝐹 ‘ 𝑥 ) E ( 𝐹 ‘ 𝑦 ) ) ) )
18 7 16 17 sylanbrc ⊢ ( ( ( Ord 𝐴 ∧ 𝐵 ⊆ On ) ∧ ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) ) → 𝐹 Isom E , E ( 𝐴 , 𝐵 ) )
19 18 ex ⊢ ( ( Ord 𝐴 ∧ 𝐵 ⊆ On ) → ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) → 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ) )
20 isof1o ⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 –1-1-onto→ 𝐵 )
21 f1ofo ⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐵 → 𝐹 : 𝐴 –onto→ 𝐵 )
22 20 21 syl ⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → 𝐹 : 𝐴 –onto→ 𝐵 )
23 22 3ad2ant1 ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On ) → 𝐹 : 𝐴 –onto→ 𝐵 )
24 smoiso ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On ) → Smo 𝐹 )
25 23 24 jca ⊢ ( ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ∧ Ord 𝐴 ∧ 𝐵 ⊆ On ) → ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) )
26 25 3expib ⊢ ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → ( ( Ord 𝐴 ∧ 𝐵 ⊆ On ) → ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) ) )
27 26 com12 ⊢ ( ( Ord 𝐴 ∧ 𝐵 ⊆ On ) → ( 𝐹 Isom E , E ( 𝐴 , 𝐵 ) → ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) ) )
28 19 27 impbid ⊢ ( ( Ord 𝐴 ∧ 𝐵 ⊆ On ) → ( ( 𝐹 : 𝐴 –onto→ 𝐵 ∧ Smo 𝐹 ) ↔ 𝐹 Isom E , E ( 𝐴 , 𝐵 ) ) )