MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  oismo Structured version   Visualization version   GIF version

Theorem oismo 8442
Description: When 𝐴 is a subclass of On, 𝐹 is a strictly monotone ordinal functions, and it is also complete (it is an isomorphism onto all of 𝐴). The proof avoids ax-rep 4769 (the second statement is trivial under ax-rep 4769). (Contributed by Mario Carneiro, 26-Jun-2015.)
Hypothesis
Ref Expression
oismo.1 𝐹 = OrdIso( E , 𝐴)
Assertion
Ref Expression
oismo (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴))

Proof of Theorem oismo
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 epweon 6980 . . . . . 6 E We On
2 wess 5099 . . . . . 6 (𝐴 ⊆ On → ( E We On → E We 𝐴))
31, 2mpi 20 . . . . 5 (𝐴 ⊆ On → E We 𝐴)
4 epse 5095 . . . . 5 E Se 𝐴
5 oismo.1 . . . . . 6 𝐹 = OrdIso( E , 𝐴)
65oiiso2 8433 . . . . 5 (( E We 𝐴 ∧ E Se 𝐴) → 𝐹 Isom E , E (dom 𝐹, ran 𝐹))
73, 4, 6sylancl 694 . . . 4 (𝐴 ⊆ On → 𝐹 Isom E , E (dom 𝐹, ran 𝐹))
85oicl 8431 . . . . 5 Ord dom 𝐹
95oif 8432 . . . . . . 7 𝐹:dom 𝐹𝐴
10 frn 6051 . . . . . . 7 (𝐹:dom 𝐹𝐴 → ran 𝐹𝐴)
119, 10ax-mp 5 . . . . . 6 ran 𝐹𝐴
12 id 22 . . . . . 6 (𝐴 ⊆ On → 𝐴 ⊆ On)
1311, 12syl5ss 3612 . . . . 5 (𝐴 ⊆ On → ran 𝐹 ⊆ On)
14 smoiso2 7463 . . . . 5 ((Ord dom 𝐹 ∧ ran 𝐹 ⊆ On) → ((𝐹:dom 𝐹onto→ran 𝐹 ∧ Smo 𝐹) ↔ 𝐹 Isom E , E (dom 𝐹, ran 𝐹)))
158, 13, 14sylancr 695 . . . 4 (𝐴 ⊆ On → ((𝐹:dom 𝐹onto→ran 𝐹 ∧ Smo 𝐹) ↔ 𝐹 Isom E , E (dom 𝐹, ran 𝐹)))
167, 15mpbird 247 . . 3 (𝐴 ⊆ On → (𝐹:dom 𝐹onto→ran 𝐹 ∧ Smo 𝐹))
1716simprd 479 . 2 (𝐴 ⊆ On → Smo 𝐹)
1811a1i 11 . . 3 (𝐴 ⊆ On → ran 𝐹𝐴)
19 simprl 794 . . . . . . . 8 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝑥𝐴)
203adantr 481 . . . . . . . . . 10 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → E We 𝐴)
214a1i 11 . . . . . . . . . 10 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → E Se 𝐴)
22 ffn 6043 . . . . . . . . . . . . 13 (𝐹:dom 𝐹𝐴𝐹 Fn dom 𝐹)
239, 22mp1i 13 . . . . . . . . . . . 12 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝐹 Fn dom 𝐹)
24 simplrr 801 . . . . . . . . . . . . . . 15 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → ¬ 𝑥 ∈ ran 𝐹)
253ad2antrr 762 . . . . . . . . . . . . . . . . 17 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → E We 𝐴)
264a1i 11 . . . . . . . . . . . . . . . . 17 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → E Se 𝐴)
27 simplrl 800 . . . . . . . . . . . . . . . . 17 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑥𝐴)
28 simpr 477 . . . . . . . . . . . . . . . . 17 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑦 ∈ dom 𝐹)
295oiiniseg 8435 . . . . . . . . . . . . . . . . 17 ((( E We 𝐴 ∧ E Se 𝐴) ∧ (𝑥𝐴𝑦 ∈ dom 𝐹)) → ((𝐹𝑦) E 𝑥𝑥 ∈ ran 𝐹))
3025, 26, 27, 28, 29syl22anc 1326 . . . . . . . . . . . . . . . 16 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → ((𝐹𝑦) E 𝑥𝑥 ∈ ran 𝐹))
3130ord 392 . . . . . . . . . . . . . . 15 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → (¬ (𝐹𝑦) E 𝑥𝑥 ∈ ran 𝐹))
3224, 31mt3d 140 . . . . . . . . . . . . . 14 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → (𝐹𝑦) E 𝑥)
33 vex 3201 . . . . . . . . . . . . . . 15 𝑥 ∈ V
3433epelc 5029 . . . . . . . . . . . . . 14 ((𝐹𝑦) E 𝑥 ↔ (𝐹𝑦) ∈ 𝑥)
3532, 34sylib 208 . . . . . . . . . . . . 13 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → (𝐹𝑦) ∈ 𝑥)
3635ralrimiva 2965 . . . . . . . . . . . 12 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → ∀𝑦 ∈ dom 𝐹(𝐹𝑦) ∈ 𝑥)
37 ffnfv 6386 . . . . . . . . . . . 12 (𝐹:dom 𝐹𝑥 ↔ (𝐹 Fn dom 𝐹 ∧ ∀𝑦 ∈ dom 𝐹(𝐹𝑦) ∈ 𝑥))
3823, 36, 37sylanbrc 698 . . . . . . . . . . 11 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝐹:dom 𝐹𝑥)
399, 22mp1i 13 . . . . . . . . . . . . . . . 16 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝐹 Fn dom 𝐹)
4017ad2antrr 762 . . . . . . . . . . . . . . . 16 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → Smo 𝐹)
41 smogt 7461 . . . . . . . . . . . . . . . 16 ((𝐹 Fn dom 𝐹 ∧ Smo 𝐹𝑦 ∈ dom 𝐹) → 𝑦 ⊆ (𝐹𝑦))
4239, 40, 28, 41syl3anc 1325 . . . . . . . . . . . . . . 15 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑦 ⊆ (𝐹𝑦))
43 ordelon 5745 . . . . . . . . . . . . . . . . 17 ((Ord dom 𝐹𝑦 ∈ dom 𝐹) → 𝑦 ∈ On)
448, 28, 43sylancr 695 . . . . . . . . . . . . . . . 16 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑦 ∈ On)
45 simpll 790 . . . . . . . . . . . . . . . . 17 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝐴 ⊆ On)
4645, 27sseldd 3602 . . . . . . . . . . . . . . . 16 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑥 ∈ On)
47 ontr2 5770 . . . . . . . . . . . . . . . 16 ((𝑦 ∈ On ∧ 𝑥 ∈ On) → ((𝑦 ⊆ (𝐹𝑦) ∧ (𝐹𝑦) ∈ 𝑥) → 𝑦𝑥))
4844, 46, 47syl2anc 693 . . . . . . . . . . . . . . 15 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → ((𝑦 ⊆ (𝐹𝑦) ∧ (𝐹𝑦) ∈ 𝑥) → 𝑦𝑥))
4942, 35, 48mp2and 715 . . . . . . . . . . . . . 14 (((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) ∧ 𝑦 ∈ dom 𝐹) → 𝑦𝑥)
5049ex 450 . . . . . . . . . . . . 13 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → (𝑦 ∈ dom 𝐹𝑦𝑥))
5150ssrdv 3607 . . . . . . . . . . . 12 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → dom 𝐹𝑥)
5219, 51ssexd 4803 . . . . . . . . . . 11 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → dom 𝐹 ∈ V)
53 fex2 7118 . . . . . . . . . . 11 ((𝐹:dom 𝐹𝑥 ∧ dom 𝐹 ∈ V ∧ 𝑥𝐴) → 𝐹 ∈ V)
5438, 52, 19, 53syl3anc 1325 . . . . . . . . . 10 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝐹 ∈ V)
555ordtype2 8436 . . . . . . . . . 10 (( E We 𝐴 ∧ E Se 𝐴𝐹 ∈ V) → 𝐹 Isom E , E (dom 𝐹, 𝐴))
5620, 21, 54, 55syl3anc 1325 . . . . . . . . 9 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝐹 Isom E , E (dom 𝐹, 𝐴))
57 isof1o 6570 . . . . . . . . 9 (𝐹 Isom E , E (dom 𝐹, 𝐴) → 𝐹:dom 𝐹1-1-onto𝐴)
58 f1ofo 6142 . . . . . . . . 9 (𝐹:dom 𝐹1-1-onto𝐴𝐹:dom 𝐹onto𝐴)
59 forn 6116 . . . . . . . . 9 (𝐹:dom 𝐹onto𝐴 → ran 𝐹 = 𝐴)
6056, 57, 58, 594syl 19 . . . . . . . 8 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → ran 𝐹 = 𝐴)
6119, 60eleqtrrd 2703 . . . . . . 7 ((𝐴 ⊆ On ∧ (𝑥𝐴 ∧ ¬ 𝑥 ∈ ran 𝐹)) → 𝑥 ∈ ran 𝐹)
6261expr 643 . . . . . 6 ((𝐴 ⊆ On ∧ 𝑥𝐴) → (¬ 𝑥 ∈ ran 𝐹𝑥 ∈ ran 𝐹))
6362pm2.18d 124 . . . . 5 ((𝐴 ⊆ On ∧ 𝑥𝐴) → 𝑥 ∈ ran 𝐹)
6463ex 450 . . . 4 (𝐴 ⊆ On → (𝑥𝐴𝑥 ∈ ran 𝐹))
6564ssrdv 3607 . . 3 (𝐴 ⊆ On → 𝐴 ⊆ ran 𝐹)
6618, 65eqssd 3618 . 2 (𝐴 ⊆ On → ran 𝐹 = 𝐴)
6717, 66jca 554 1 (𝐴 ⊆ On → (Smo 𝐹 ∧ ran 𝐹 = 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1482  wcel 1989  wral 2911  Vcvv 3198  wss 3572   class class class wbr 4651   E cep 5026   Se wse 5069   We wwe 5070  dom cdm 5112  ran crn 5113  Ord word 5720  Oncon0 5721   Fn wfn 5881  wf 5882  ontowfo 5884  1-1-ontowf1o 5885  cfv 5886   Isom wiso 5887  Smo wsmo 7439  OrdIsocoi 8411
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pow 4841  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-ne 2794  df-ral 2916  df-rex 2917  df-reu 2918  df-rmo 2919  df-rab 2920  df-v 3200  df-sbc 3434  df-csb 3532  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-pss 3588  df-nul 3914  df-if 4085  df-pw 4158  df-sn 4176  df-pr 4178  df-tp 4180  df-op 4182  df-uni 4435  df-iun 4520  df-br 4652  df-opab 4711  df-mpt 4728  df-tr 4751  df-id 5022  df-eprel 5027  df-po 5033  df-so 5034  df-fr 5071  df-se 5072  df-we 5073  df-xp 5118  df-rel 5119  df-cnv 5120  df-co 5121  df-dm 5122  df-rn 5123  df-res 5124  df-ima 5125  df-pred 5678  df-ord 5724  df-on 5725  df-lim 5726  df-suc 5727  df-iota 5849  df-fun 5888  df-fn 5889  df-f 5890  df-f1 5891  df-fo 5892  df-f1o 5893  df-fv 5894  df-isom 5895  df-riota 6608  df-wrecs 7404  df-smo 7440  df-recs 7465  df-oi 8412
This theorem is referenced by:  oiid  8443  hsmexlem1  9245  hsmexlem2  9246
  Copyright terms: Public domain W3C validator