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

Theorem ordtypelem9 9467
Description: Lemma for ordtype 9473. Either the function OrdIso is an isomorphism onto all of 𝐴, or OrdIso is not a set, which by oif 9471 implies that either ran 𝑂𝐴 is a proper class or dom 𝑂 = On. (Contributed by Mario Carneiro, 25-Jun-2015.) (Revised by AV, 28-Jul-2024.)
Hypotheses
Ref Expression
ordtypelem.1 𝐹 = recs(𝐺)
ordtypelem.2 𝐶 = {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
ordtypelem.3 𝐺 = ( ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑅𝑣))
ordtypelem.5 𝑇 = {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡}
ordtypelem.6 𝑂 = OrdIso(𝑅, 𝐴)
ordtypelem.7 (𝜑𝑅 We 𝐴)
ordtypelem.8 (𝜑𝑅 Se 𝐴)
ordtypelem9.1 (𝜑𝑂𝑉)
Assertion
Ref Expression
ordtypelem9 (𝜑𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
Distinct variable groups:   𝑣,𝑢,𝐶   ,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧,𝑅   𝐴,,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧   𝑡,𝑂,𝑢,𝑣,𝑥   𝜑,𝑡,𝑥   ,𝐹,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑤,𝑣,𝑢,,𝑗)   𝐶(𝑥,𝑧,𝑤,𝑡,,𝑗)   𝑇(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,,𝑗)   𝐺(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,,𝑗)   𝑂(𝑧,𝑤,,𝑗)   𝑉(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,,𝑗)

Proof of Theorem ordtypelem9
Dummy variables 𝑎 𝑏 𝑐 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordtypelem.1 . . 3 𝐹 = recs(𝐺)
2 ordtypelem.2 . . 3 𝐶 = {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
3 ordtypelem.3 . . 3 𝐺 = ( ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑅𝑣))
4 ordtypelem.5 . . 3 𝑇 = {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡}
5 ordtypelem.6 . . 3 𝑂 = OrdIso(𝑅, 𝐴)
6 ordtypelem.7 . . 3 (𝜑𝑅 We 𝐴)
7 ordtypelem.8 . . 3 (𝜑𝑅 Se 𝐴)
81, 2, 3, 4, 5, 6, 7ordtypelem8 9466 . 2 (𝜑𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂))
91, 2, 3, 4, 5, 6, 7ordtypelem4 9462 . . . . 5 (𝜑𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
109frnd 6677 . . . 4 (𝜑 → ran 𝑂𝐴)
111, 2, 3, 4, 5, 6, 7ordtypelem2 9460 . . . . . . . . . . 11 (𝜑 → Ord 𝑇)
12 ordirr 6336 . . . . . . . . . . 11 (Ord 𝑇 → ¬ 𝑇𝑇)
1311, 12syl 17 . . . . . . . . . 10 (𝜑 → ¬ 𝑇𝑇)
141tfr1a 8341 . . . . . . . . . . . . . 14 (Fun 𝐹 ∧ Lim dom 𝐹)
1514simpri 487 . . . . . . . . . . . . 13 Lim dom 𝐹
16 limord 6378 . . . . . . . . . . . . 13 (Lim dom 𝐹 → Ord dom 𝐹)
1715, 16ax-mp 5 . . . . . . . . . . . 12 Ord dom 𝐹
181, 2, 3, 4, 5, 6, 7ordtypelem1 9459 . . . . . . . . . . . . . 14 (𝜑𝑂 = (𝐹𝑇))
19 ordtypelem9.1 . . . . . . . . . . . . . . 15 (𝜑𝑂𝑉)
2019elexd 3464 . . . . . . . . . . . . . 14 (𝜑𝑂 ∈ V)
2118, 20eqeltrrd 2835 . . . . . . . . . . . . 13 (𝜑 → (𝐹𝑇) ∈ V)
221tfr2b 8343 . . . . . . . . . . . . . 14 (Ord 𝑇 → (𝑇 ∈ dom 𝐹 ↔ (𝐹𝑇) ∈ V))
2311, 22syl 17 . . . . . . . . . . . . 13 (𝜑 → (𝑇 ∈ dom 𝐹 ↔ (𝐹𝑇) ∈ V))
2421, 23mpbird 257 . . . . . . . . . . . 12 (𝜑𝑇 ∈ dom 𝐹)
25 ordelon 6342 . . . . . . . . . . . 12 ((Ord dom 𝐹𝑇 ∈ dom 𝐹) → 𝑇 ∈ On)
2617, 24, 25sylancr 588 . . . . . . . . . . 11 (𝜑𝑇 ∈ On)
27 imaeq2 6010 . . . . . . . . . . . . . . 15 (𝑎 = 𝑇 → (𝐹𝑎) = (𝐹𝑇))
2827raleqdv 3312 . . . . . . . . . . . . . 14 (𝑎 = 𝑇 → (∀𝑐 ∈ (𝐹𝑎)𝑐𝑅𝑏 ↔ ∀𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏))
2928rexbidv 3172 . . . . . . . . . . . . 13 (𝑎 = 𝑇 → (∃𝑏𝐴𝑐 ∈ (𝐹𝑎)𝑐𝑅𝑏 ↔ ∃𝑏𝐴𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏))
30 breq1 5109 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑐 → (𝑧𝑅𝑡𝑐𝑅𝑡))
3130cbvralvw 3224 . . . . . . . . . . . . . . . . . 18 (∀𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡 ↔ ∀𝑐 ∈ (𝐹𝑥)𝑐𝑅𝑡)
32 breq2 5110 . . . . . . . . . . . . . . . . . . 19 (𝑡 = 𝑏 → (𝑐𝑅𝑡𝑐𝑅𝑏))
3332ralbidv 3171 . . . . . . . . . . . . . . . . . 18 (𝑡 = 𝑏 → (∀𝑐 ∈ (𝐹𝑥)𝑐𝑅𝑡 ↔ ∀𝑐 ∈ (𝐹𝑥)𝑐𝑅𝑏))
3431, 33bitrid 283 . . . . . . . . . . . . . . . . 17 (𝑡 = 𝑏 → (∀𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡 ↔ ∀𝑐 ∈ (𝐹𝑥)𝑐𝑅𝑏))
3534cbvrexvw 3225 . . . . . . . . . . . . . . . 16 (∃𝑡𝐴𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡 ↔ ∃𝑏𝐴𝑐 ∈ (𝐹𝑥)𝑐𝑅𝑏)
36 imaeq2 6010 . . . . . . . . . . . . . . . . . 18 (𝑥 = 𝑎 → (𝐹𝑥) = (𝐹𝑎))
3736raleqdv 3312 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑎 → (∀𝑐 ∈ (𝐹𝑥)𝑐𝑅𝑏 ↔ ∀𝑐 ∈ (𝐹𝑎)𝑐𝑅𝑏))
3837rexbidv 3172 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑎 → (∃𝑏𝐴𝑐 ∈ (𝐹𝑥)𝑐𝑅𝑏 ↔ ∃𝑏𝐴𝑐 ∈ (𝐹𝑎)𝑐𝑅𝑏))
3935, 38bitrid 283 . . . . . . . . . . . . . . 15 (𝑥 = 𝑎 → (∃𝑡𝐴𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡 ↔ ∃𝑏𝐴𝑐 ∈ (𝐹𝑎)𝑐𝑅𝑏))
4039cbvrabv 3416 . . . . . . . . . . . . . 14 {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡} = {𝑎 ∈ On ∣ ∃𝑏𝐴𝑐 ∈ (𝐹𝑎)𝑐𝑅𝑏}
414, 40eqtri 2761 . . . . . . . . . . . . 13 𝑇 = {𝑎 ∈ On ∣ ∃𝑏𝐴𝑐 ∈ (𝐹𝑎)𝑐𝑅𝑏}
4229, 41elrab2 3649 . . . . . . . . . . . 12 (𝑇𝑇 ↔ (𝑇 ∈ On ∧ ∃𝑏𝐴𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏))
4342baib 537 . . . . . . . . . . 11 (𝑇 ∈ On → (𝑇𝑇 ↔ ∃𝑏𝐴𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏))
4426, 43syl 17 . . . . . . . . . 10 (𝜑 → (𝑇𝑇 ↔ ∃𝑏𝐴𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏))
4513, 44mtbid 324 . . . . . . . . 9 (𝜑 → ¬ ∃𝑏𝐴𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏)
46 ralnex 3072 . . . . . . . . 9 (∀𝑏𝐴 ¬ ∀𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏 ↔ ¬ ∃𝑏𝐴𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏)
4745, 46sylibr 233 . . . . . . . 8 (𝜑 → ∀𝑏𝐴 ¬ ∀𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏)
4847r19.21bi 3233 . . . . . . 7 ((𝜑𝑏𝐴) → ¬ ∀𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏)
4918rneqd 5894 . . . . . . . . . . 11 (𝜑 → ran 𝑂 = ran (𝐹𝑇))
50 df-ima 5647 . . . . . . . . . . 11 (𝐹𝑇) = ran (𝐹𝑇)
5149, 50eqtr4di 2791 . . . . . . . . . 10 (𝜑 → ran 𝑂 = (𝐹𝑇))
5251adantr 482 . . . . . . . . 9 ((𝜑𝑏𝐴) → ran 𝑂 = (𝐹𝑇))
5352raleqdv 3312 . . . . . . . 8 ((𝜑𝑏𝐴) → (∀𝑐 ∈ ran 𝑂 𝑐𝑅𝑏 ↔ ∀𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏))
549ffund 6673 . . . . . . . . . . 11 (𝜑 → Fun 𝑂)
5554funfnd 6533 . . . . . . . . . 10 (𝜑𝑂 Fn dom 𝑂)
5655adantr 482 . . . . . . . . 9 ((𝜑𝑏𝐴) → 𝑂 Fn dom 𝑂)
57 breq1 5109 . . . . . . . . . 10 (𝑐 = (𝑂𝑚) → (𝑐𝑅𝑏 ↔ (𝑂𝑚)𝑅𝑏))
5857ralrn 7039 . . . . . . . . 9 (𝑂 Fn dom 𝑂 → (∀𝑐 ∈ ran 𝑂 𝑐𝑅𝑏 ↔ ∀𝑚 ∈ dom 𝑂(𝑂𝑚)𝑅𝑏))
5956, 58syl 17 . . . . . . . 8 ((𝜑𝑏𝐴) → (∀𝑐 ∈ ran 𝑂 𝑐𝑅𝑏 ↔ ∀𝑚 ∈ dom 𝑂(𝑂𝑚)𝑅𝑏))
6053, 59bitr3d 281 . . . . . . 7 ((𝜑𝑏𝐴) → (∀𝑐 ∈ (𝐹𝑇)𝑐𝑅𝑏 ↔ ∀𝑚 ∈ dom 𝑂(𝑂𝑚)𝑅𝑏))
6148, 60mtbid 324 . . . . . 6 ((𝜑𝑏𝐴) → ¬ ∀𝑚 ∈ dom 𝑂(𝑂𝑚)𝑅𝑏)
62 rexnal 3100 . . . . . 6 (∃𝑚 ∈ dom 𝑂 ¬ (𝑂𝑚)𝑅𝑏 ↔ ¬ ∀𝑚 ∈ dom 𝑂(𝑂𝑚)𝑅𝑏)
6361, 62sylibr 233 . . . . 5 ((𝜑𝑏𝐴) → ∃𝑚 ∈ dom 𝑂 ¬ (𝑂𝑚)𝑅𝑏)
641, 2, 3, 4, 5, 6, 7ordtypelem7 9465 . . . . . . 7 (((𝜑𝑏𝐴) ∧ 𝑚 ∈ dom 𝑂) → ((𝑂𝑚)𝑅𝑏𝑏 ∈ ran 𝑂))
6564ord 863 . . . . . 6 (((𝜑𝑏𝐴) ∧ 𝑚 ∈ dom 𝑂) → (¬ (𝑂𝑚)𝑅𝑏𝑏 ∈ ran 𝑂))
6665rexlimdva 3149 . . . . 5 ((𝜑𝑏𝐴) → (∃𝑚 ∈ dom 𝑂 ¬ (𝑂𝑚)𝑅𝑏𝑏 ∈ ran 𝑂))
6763, 66mpd 15 . . . 4 ((𝜑𝑏𝐴) → 𝑏 ∈ ran 𝑂)
6810, 67eqelssd 3966 . . 3 (𝜑 → ran 𝑂 = 𝐴)
69 isoeq5 7267 . . 3 (ran 𝑂 = 𝐴 → (𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂) ↔ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)))
7068, 69syl 17 . 2 (𝜑 → (𝑂 Isom E , 𝑅 (dom 𝑂, ran 𝑂) ↔ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)))
718, 70mpbid 231 1 (𝜑𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 397   = wceq 1542  wcel 2107  wral 3061  wrex 3070  {crab 3406  Vcvv 3444  cin 3910   class class class wbr 5106  cmpt 5189   E cep 5537   Se wse 5587   We wwe 5588  dom cdm 5634  ran crn 5635  cres 5636  cima 5637  Ord word 6317  Oncon0 6318  Lim wlim 6319  Fun wfun 6491   Fn wfn 6492  cfv 6497   Isom wiso 6498  crio 7313  recscrecs 8317  OrdIsocoi 9450
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5257  ax-nul 5264  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3930  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-tr 5224  df-id 5532  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5589  df-se 5590  df-we 5591  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6254  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-isom 6506  df-riota 7314  df-ov 7361  df-2nd 7923  df-frecs 8213  df-wrecs 8244  df-recs 8318  df-oi 9451
This theorem is referenced by:  ordtypelem10  9468  ordtype2  9475
  Copyright terms: Public domain W3C validator