Metamath Proof Explorer

Theorem oismo

Description: When A is a subclass of On , F is a strictly monotone ordinal functions, and it is also complete (it is an isomorphism onto all of A ). The proof avoids ax-rep (the second statement is trivial under ax-rep ). (Contributed by Mario Carneiro, 26-Jun-2015)

Ref Expression
Hypothesis oismo.1 ⊢ 𝐹 = OrdIso ( E , 𝐴 )
Assertion oismo ( 𝐴 ⊆ On → ( Smo 𝐹 ∧ ran 𝐹 = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 oismo.1 ⊢ 𝐹 = OrdIso ( E , 𝐴 )
2 epweon ⊢ E We On
3 wess ⊢ ( 𝐴 ⊆ On → ( E We On → E We 𝐴 ) )
4 2 3 mpi ⊢ ( 𝐴 ⊆ On → E We 𝐴 )
5 epse ⊢ E Se 𝐴
6 1 oiiso2 ⊢ ( ( E We 𝐴 ∧ E Se 𝐴 ) → 𝐹 Isom E , E ( dom 𝐹 , ran 𝐹 ) )
7 4 5 6 sylancl ⊢ ( 𝐴 ⊆ On → 𝐹 Isom E , E ( dom 𝐹 , ran 𝐹 ) )
8 1 oicl ⊢ Ord dom 𝐹
9 1 oif ⊢ 𝐹 : dom 𝐹 ⟶ 𝐴
10 frn ⊢ ( 𝐹 : dom 𝐹 ⟶ 𝐴 → ran 𝐹 ⊆ 𝐴 )
11 9 10 ax-mp ⊢ ran 𝐹 ⊆ 𝐴
12 id ⊢ ( 𝐴 ⊆ On → 𝐴 ⊆ On )
13 11 12 sstrid ⊢ ( 𝐴 ⊆ On → ran 𝐹 ⊆ On )
14 smoiso2 ⊢ ( ( Ord dom 𝐹 ∧ ran 𝐹 ⊆ On ) → ( ( 𝐹 : dom 𝐹 –onto→ ran 𝐹 ∧ Smo 𝐹 ) ↔ 𝐹 Isom E , E ( dom 𝐹 , ran 𝐹 ) ) )
15 8 13 14 sylancr ⊢ ( 𝐴 ⊆ On → ( ( 𝐹 : dom 𝐹 –onto→ ran 𝐹 ∧ Smo 𝐹 ) ↔ 𝐹 Isom E , E ( dom 𝐹 , ran 𝐹 ) ) )
16 7 15 mpbird ⊢ ( 𝐴 ⊆ On → ( 𝐹 : dom 𝐹 –onto→ ran 𝐹 ∧ Smo 𝐹 ) )
17 16 simprd ⊢ ( 𝐴 ⊆ On → Smo 𝐹 )
18 11 a1i ⊢ ( 𝐴 ⊆ On → ran 𝐹 ⊆ 𝐴 )
19 simprl ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → 𝑥 ∈ 𝐴 )
20 4 adantr ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → E We 𝐴 )
21 5 a1i ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → E Se 𝐴 )
22 ffn ⊢ ( 𝐹 : dom 𝐹 ⟶ 𝐴 → 𝐹 Fn dom 𝐹 )
23 9 22 mp1i ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → 𝐹 Fn dom 𝐹 )
24 simplrr ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → ¬ 𝑥 ∈ ran 𝐹 )
25 4 ad2antrr ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → E We 𝐴 )
26 5 a1i ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → E Se 𝐴 )
27 simplrl ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → 𝑥 ∈ 𝐴 )
28 simpr ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → 𝑦 ∈ dom 𝐹 )
29 1 oiiniseg ⊢ ( ( ( E We 𝐴 ∧ E Se 𝐴 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ dom 𝐹 ) ) → ( ( 𝐹 ‘ 𝑦 ) E 𝑥 ∨ 𝑥 ∈ ran 𝐹 ) )
30 25 26 27 28 29 syl22anc ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝑦 ) E 𝑥 ∨ 𝑥 ∈ ran 𝐹 ) )
31 30 ord ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → ( ¬ ( 𝐹 ‘ 𝑦 ) E 𝑥 → 𝑥 ∈ ran 𝐹 ) )
32 24 31 mt3d ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) E 𝑥 )
33 epel ⊢ ( ( 𝐹 ‘ 𝑦 ) E 𝑥 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 )
34 32 33 sylib ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 )
35 34 ralrimiva ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → ∀ 𝑦 ∈ dom 𝐹 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 )
36 ffnfv ⊢ ( 𝐹 : dom 𝐹 ⟶ 𝑥 ↔ ( 𝐹 Fn dom 𝐹 ∧ ∀ 𝑦 ∈ dom 𝐹 ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) )
37 23 35 36 sylanbrc ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → 𝐹 : dom 𝐹 ⟶ 𝑥 )
38 9 22 mp1i ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → 𝐹 Fn dom 𝐹 )
39 17 ad2antrr ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → Smo 𝐹 )
40 smogt ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ Smo 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) )
41 38 39 28 40 syl3anc ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) )
42 ordelon ⊢ ( ( Ord dom 𝐹 ∧ 𝑦 ∈ dom 𝐹 ) → 𝑦 ∈ On )
43 8 28 42 sylancr ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → 𝑦 ∈ On )
44 simpll ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → 𝐴 ⊆ On )
45 44 27 sseldd ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → 𝑥 ∈ On )
46 ontr2 ⊢ ( ( 𝑦 ∈ On ∧ 𝑥 ∈ On ) → ( ( 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) → 𝑦 ∈ 𝑥 ) )
47 43 45 46 syl2anc ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → ( ( 𝑦 ⊆ ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑥 ) → 𝑦 ∈ 𝑥 ) )
48 41 34 47 mp2and ⊢ ( ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) ∧ 𝑦 ∈ dom 𝐹 ) → 𝑦 ∈ 𝑥 )
49 48 ex ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → ( 𝑦 ∈ dom 𝐹 → 𝑦 ∈ 𝑥 ) )
50 49 ssrdv ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → dom 𝐹 ⊆ 𝑥 )
51 19 50 ssexd ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → dom 𝐹 ∈ V )
52 fex2 ⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝑥 ∧ dom 𝐹 ∈ V ∧ 𝑥 ∈ 𝐴 ) → 𝐹 ∈ V )
53 37 51 19 52 syl3anc ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → 𝐹 ∈ V )
54 1 ordtype2 ⊢ ( ( E We 𝐴 ∧ E Se 𝐴 ∧ 𝐹 ∈ V ) → 𝐹 Isom E , E ( dom 𝐹 , 𝐴 ) )
55 20 21 53 54 syl3anc ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → 𝐹 Isom E , E ( dom 𝐹 , 𝐴 ) )
56 isof1o ⊢ ( 𝐹 Isom E , E ( dom 𝐹 , 𝐴 ) → 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 )
57 f1ofo ⊢ ( 𝐹 : dom 𝐹 –1-1-onto→ 𝐴 → 𝐹 : dom 𝐹 –onto→ 𝐴 )
58 forn ⊢ ( 𝐹 : dom 𝐹 –onto→ 𝐴 → ran 𝐹 = 𝐴 )
59 55 56 57 58 4syl ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → ran 𝐹 = 𝐴 )
60 19 59 eleqtrrd ⊢ ( ( 𝐴 ⊆ On ∧ ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹 ) ) → 𝑥 ∈ ran 𝐹 )
61 60 expr ⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → ( ¬ 𝑥 ∈ ran 𝐹 → 𝑥 ∈ ran 𝐹 ) )
62 61 pm2.18d ⊢ ( ( 𝐴 ⊆ On ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ran 𝐹 )
63 18 62 eqelssd ⊢ ( 𝐴 ⊆ On → ran 𝐹 = 𝐴 )
64 17 63 jca ⊢ ( 𝐴 ⊆ On → ( Smo 𝐹 ∧ ran 𝐹 = 𝐴 ) )