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

Theorem oif 9317
Description: The order isomorphism of the well-order 𝑅 on 𝐴 is a function. (Contributed by Mario Carneiro, 23-May-2015.)
Hypothesis
Ref Expression
oicl.1 𝐹 = OrdIso(𝑅, 𝐴)
Assertion
Ref Expression
oif 𝐹:dom 𝐹𝐴

Proof of Theorem oif
Dummy variables 𝑢 𝑡 𝑣 𝑥 𝑗 𝑤 𝑧 𝑓 𝑖 𝑟 𝑠 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2733 . . . . 5 recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))) = recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)))
2 eqid 2733 . . . . 5 {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} = {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
3 eqid 2733 . . . . 5 ( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)) = ( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
41, 2, 3ordtypecbv 9304 . . . 4 recs((𝑓 ∈ V ↦ (𝑠 ∈ {𝑦𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦}∀𝑟 ∈ {𝑦𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦} ¬ 𝑟𝑅𝑠))) = recs(( ∈ V ↦ (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)))
5 eqid 2733 . . . 4 {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs((𝑓 ∈ V ↦ (𝑠 ∈ {𝑦𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦}∀𝑟 ∈ {𝑦𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦} ¬ 𝑟𝑅𝑠))) “ 𝑥)𝑧𝑅𝑡} = {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (recs((𝑓 ∈ V ↦ (𝑠 ∈ {𝑦𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦}∀𝑟 ∈ {𝑦𝐴 ∣ ∀𝑖 ∈ ran 𝑓 𝑖𝑅𝑦} ¬ 𝑟𝑅𝑠))) “ 𝑥)𝑧𝑅𝑡}
6 oicl.1 . . . 4 𝐹 = OrdIso(𝑅, 𝐴)
7 simpl 482 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴) → 𝑅 We 𝐴)
8 simpr 484 . . . 4 ((𝑅 We 𝐴𝑅 Se 𝐴) → 𝑅 Se 𝐴)
94, 2, 3, 5, 6, 7, 8ordtypelem5 9309 . . 3 ((𝑅 We 𝐴𝑅 Se 𝐴) → (Ord dom 𝐹𝐹:dom 𝐹𝐴))
109simprd 495 . 2 ((𝑅 We 𝐴𝑅 Se 𝐴) → 𝐹:dom 𝐹𝐴)
11 f0 6673 . . 3 ∅:∅⟶𝐴
126oi0 9315 . . . 4 (¬ (𝑅 We 𝐴𝑅 Se 𝐴) → 𝐹 = ∅)
1312dmeqd 5818 . . . . 5 (¬ (𝑅 We 𝐴𝑅 Se 𝐴) → dom 𝐹 = dom ∅)
14 dm0 5833 . . . . 5 dom ∅ = ∅
1513, 14eqtrdi 2789 . . . 4 (¬ (𝑅 We 𝐴𝑅 Se 𝐴) → dom 𝐹 = ∅)
1612, 15feq12d 6606 . . 3 (¬ (𝑅 We 𝐴𝑅 Se 𝐴) → (𝐹:dom 𝐹𝐴 ↔ ∅:∅⟶𝐴))
1711, 16mpbiri 257 . 2 (¬ (𝑅 We 𝐴𝑅 Se 𝐴) → 𝐹:dom 𝐹𝐴)
1810, 17pm2.61i 182 1 𝐹:dom 𝐹𝐴
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wa 395   = wceq 1537  wral 3059  wrex 3068  {crab 3221  Vcvv 3434  c0 4259   class class class wbr 5077  cmpt 5160   Se wse 5544   We wwe 5545  dom cdm 5591  ran crn 5592  cima 5594  Ord word 6269  Oncon0 6270  wf 6443  crio 7251  recscrecs 8221  OrdIsocoi 9296
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2103  ax-9 2111  ax-10 2132  ax-11 2149  ax-12 2166  ax-ext 2704  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-un 7608
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2063  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2884  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3222  df-reu 3223  df-rab 3224  df-v 3436  df-sbc 3719  df-csb 3835  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-pss 3908  df-nul 4260  df-if 4463  df-pw 4538  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4842  df-iun 4929  df-br 5078  df-opab 5140  df-mpt 5161  df-tr 5195  df-id 5491  df-eprel 5497  df-po 5505  df-so 5506  df-fr 5546  df-se 5547  df-we 5548  df-xp 5597  df-rel 5598  df-cnv 5599  df-co 5600  df-dm 5601  df-rn 5602  df-res 5603  df-ima 5604  df-pred 6206  df-ord 6273  df-on 6274  df-lim 6275  df-suc 6276  df-iota 6399  df-fun 6449  df-fn 6450  df-f 6451  df-f1 6452  df-fo 6453  df-f1o 6454  df-fv 6455  df-riota 7252  df-ov 7298  df-2nd 7852  df-frecs 8117  df-wrecs 8148  df-recs 8222  df-oi 9297
This theorem is referenced by:  oismo  9327  cantnfle  9457  cantnflt  9458  cantnfres  9463  cantnfp1lem3  9466  cantnflem1b  9472  cantnflem1  9475  wemapwe  9483  cnfcomlem  9485  cnfcom  9486  cnfcom3lem  9489  cnfcom3  9490  hsmexlem1  10210  hsmexlem2  10211  fpwwe2lem7  10421
  Copyright terms: Public domain W3C validator