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

Theorem smoiso 7504
Description: If 𝐹 is an isomorphism from an ordinal 𝐴 onto 𝐵, which is a subset of the ordinals, then 𝐹 is a strictly monotonic function. Exercise 3 in [TakeutiZaring] p. 50. (Contributed by Andrew Salmon, 24-Nov-2011.)
Assertion
Ref Expression
smoiso ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴𝐵 ⊆ On) → Smo 𝐹)

Proof of Theorem smoiso
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isof1o 6613 . . . 4 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴1-1-onto𝐵)
2 f1of 6175 . . . 4 (𝐹:𝐴1-1-onto𝐵𝐹:𝐴𝐵)
31, 2syl 17 . . 3 (𝐹 Isom E , E (𝐴, 𝐵) → 𝐹:𝐴𝐵)
4 ffdm 6100 . . . . . 6 (𝐹:𝐴𝐵 → (𝐹:dom 𝐹𝐵 ∧ dom 𝐹𝐴))
54simpld 474 . . . . 5 (𝐹:𝐴𝐵𝐹:dom 𝐹𝐵)
6 fss 6094 . . . . 5 ((𝐹:dom 𝐹𝐵𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On)
75, 6sylan 487 . . . 4 ((𝐹:𝐴𝐵𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On)
873adant2 1100 . . 3 ((𝐹:𝐴𝐵 ∧ Ord 𝐴𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On)
93, 8syl3an1 1399 . 2 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴𝐵 ⊆ On) → 𝐹:dom 𝐹⟶On)
10 fdm 6089 . . . . . 6 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
1110eqcomd 2657 . . . . 5 (𝐹:𝐴𝐵𝐴 = dom 𝐹)
12 ordeq 5768 . . . . 5 (𝐴 = dom 𝐹 → (Ord 𝐴 ↔ Ord dom 𝐹))
131, 2, 11, 124syl 19 . . . 4 (𝐹 Isom E , E (𝐴, 𝐵) → (Ord 𝐴 ↔ Ord dom 𝐹))
1413biimpa 500 . . 3 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴) → Ord dom 𝐹)
15143adant3 1101 . 2 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴𝐵 ⊆ On) → Ord dom 𝐹)
1610eleq2d 2716 . . . . . . 7 (𝐹:𝐴𝐵 → (𝑥 ∈ dom 𝐹𝑥𝐴))
1710eleq2d 2716 . . . . . . 7 (𝐹:𝐴𝐵 → (𝑦 ∈ dom 𝐹𝑦𝐴))
1816, 17anbi12d 747 . . . . . 6 (𝐹:𝐴𝐵 → ((𝑥 ∈ dom 𝐹𝑦 ∈ dom 𝐹) ↔ (𝑥𝐴𝑦𝐴)))
191, 2, 183syl 18 . . . . 5 (𝐹 Isom E , E (𝐴, 𝐵) → ((𝑥 ∈ dom 𝐹𝑦 ∈ dom 𝐹) ↔ (𝑥𝐴𝑦𝐴)))
20 isorel 6616 . . . . . . . 8 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥𝐴𝑦𝐴)) → (𝑥 E 𝑦 ↔ (𝐹𝑥) E (𝐹𝑦)))
21 epel 5061 . . . . . . . 8 (𝑥 E 𝑦𝑥𝑦)
22 fvex 6239 . . . . . . . . 9 (𝐹𝑦) ∈ V
2322epelc 5060 . . . . . . . 8 ((𝐹𝑥) E (𝐹𝑦) ↔ (𝐹𝑥) ∈ (𝐹𝑦))
2420, 21, 233bitr3g 302 . . . . . . 7 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥𝐴𝑦𝐴)) → (𝑥𝑦 ↔ (𝐹𝑥) ∈ (𝐹𝑦)))
2524biimpd 219 . . . . . 6 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ (𝑥𝐴𝑦𝐴)) → (𝑥𝑦 → (𝐹𝑥) ∈ (𝐹𝑦)))
2625ex 449 . . . . 5 (𝐹 Isom E , E (𝐴, 𝐵) → ((𝑥𝐴𝑦𝐴) → (𝑥𝑦 → (𝐹𝑥) ∈ (𝐹𝑦))))
2719, 26sylbid 230 . . . 4 (𝐹 Isom E , E (𝐴, 𝐵) → ((𝑥 ∈ dom 𝐹𝑦 ∈ dom 𝐹) → (𝑥𝑦 → (𝐹𝑥) ∈ (𝐹𝑦))))
2827ralrimivv 2999 . . 3 (𝐹 Isom E , E (𝐴, 𝐵) → ∀𝑥 ∈ dom 𝐹𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑥) ∈ (𝐹𝑦)))
29283ad2ant1 1102 . 2 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴𝐵 ⊆ On) → ∀𝑥 ∈ dom 𝐹𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑥) ∈ (𝐹𝑦)))
30 df-smo 7488 . 2 (Smo 𝐹 ↔ (𝐹:dom 𝐹⟶On ∧ Ord dom 𝐹 ∧ ∀𝑥 ∈ dom 𝐹𝑦 ∈ dom 𝐹(𝑥𝑦 → (𝐹𝑥) ∈ (𝐹𝑦))))
319, 15, 29, 30syl3anbrc 1265 1 ((𝐹 Isom E , E (𝐴, 𝐵) ∧ Ord 𝐴𝐵 ⊆ On) → Smo 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wral 2941  wss 3607   class class class wbr 4685   E cep 5057  dom cdm 5143  Ord word 5760  Oncon0 5761  wf 5922  1-1-ontowf1o 5925  cfv 5926   Isom wiso 5927  Smo wsmo 7487
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-tr 4786  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-ord 5764  df-iota 5889  df-fn 5929  df-f 5930  df-f1 5931  df-f1o 5933  df-fv 5934  df-isom 5935  df-smo 7488
This theorem is referenced by:  smoiso2  7511
  Copyright terms: Public domain W3C validator