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

Theorem ordtypelem6 8979
 Description: Lemma for ordtype 8988. (Contributed by Mario Carneiro, 24-Jun-2015.)
Hypotheses
Ref Expression
ordtypelem.1 𝐹 = recs(𝐺)
ordtypelem.2 𝐶 = {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
ordtypelem.3 𝐺 = ( ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑅𝑣))
ordtypelem.5 𝑇 = {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡}
ordtypelem.6 𝑂 = OrdIso(𝑅, 𝐴)
ordtypelem.7 (𝜑𝑅 We 𝐴)
ordtypelem.8 (𝜑𝑅 Se 𝐴)
Assertion
Ref Expression
ordtypelem6 ((𝜑𝑀 ∈ dom 𝑂) → (𝑁𝑀 → (𝑂𝑁)𝑅(𝑂𝑀)))
Distinct variable groups:   𝑣,𝑢,𝐶   ,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧,𝑀   𝑗,𝑁,𝑢,𝑤   𝑅,,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧   𝐴,,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧   𝑡,𝑂,𝑢,𝑣,𝑥   𝜑,𝑡,𝑥   ,𝐹,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑤,𝑣,𝑢,,𝑗)   𝐶(𝑥,𝑧,𝑤,𝑡,,𝑗)   𝑇(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,,𝑗)   𝐺(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,,𝑗)   𝑁(𝑥,𝑧,𝑣,𝑡,)   𝑂(𝑧,𝑤,,𝑗)

Proof of Theorem ordtypelem6
Dummy variable 𝑎 is distinct from all other variables.
StepHypRef Expression
1 fveq2 6663 . . . . 5 (𝑎 = 𝑁 → (𝐹𝑎) = (𝐹𝑁))
21breq1d 5067 . . . 4 (𝑎 = 𝑁 → ((𝐹𝑎)𝑅(𝐹𝑀) ↔ (𝐹𝑁)𝑅(𝐹𝑀)))
3 ssrab2 4054 . . . . . . . 8 {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣} ⊆ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}
4 simpr 487 . . . . . . . . . 10 ((𝜑𝑀 ∈ dom 𝑂) → 𝑀 ∈ dom 𝑂)
5 ordtypelem.1 . . . . . . . . . . . . 13 𝐹 = recs(𝐺)
6 ordtypelem.2 . . . . . . . . . . . . 13 𝐶 = {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
7 ordtypelem.3 . . . . . . . . . . . . 13 𝐺 = ( ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑅𝑣))
8 ordtypelem.5 . . . . . . . . . . . . 13 𝑇 = {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡}
9 ordtypelem.6 . . . . . . . . . . . . 13 𝑂 = OrdIso(𝑅, 𝐴)
10 ordtypelem.7 . . . . . . . . . . . . 13 (𝜑𝑅 We 𝐴)
11 ordtypelem.8 . . . . . . . . . . . . 13 (𝜑𝑅 Se 𝐴)
125, 6, 7, 8, 9, 10, 11ordtypelem4 8977 . . . . . . . . . . . 12 (𝜑𝑂:(𝑇 ∩ dom 𝐹)⟶𝐴)
1312fdmd 6516 . . . . . . . . . . 11 (𝜑 → dom 𝑂 = (𝑇 ∩ dom 𝐹))
1413adantr 483 . . . . . . . . . 10 ((𝜑𝑀 ∈ dom 𝑂) → dom 𝑂 = (𝑇 ∩ dom 𝐹))
154, 14eleqtrd 2913 . . . . . . . . 9 ((𝜑𝑀 ∈ dom 𝑂) → 𝑀 ∈ (𝑇 ∩ dom 𝐹))
165, 6, 7, 8, 9, 10, 11ordtypelem3 8976 . . . . . . . . 9 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑀) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
1715, 16syldan 593 . . . . . . . 8 ((𝜑𝑀 ∈ dom 𝑂) → (𝐹𝑀) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
183, 17sseldi 3963 . . . . . . 7 ((𝜑𝑀 ∈ dom 𝑂) → (𝐹𝑀) ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤})
19 breq2 5061 . . . . . . . . . 10 (𝑤 = (𝐹𝑀) → (𝑗𝑅𝑤𝑗𝑅(𝐹𝑀)))
2019ralbidv 3195 . . . . . . . . 9 (𝑤 = (𝐹𝑀) → (∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅(𝐹𝑀)))
2120elrab 3678 . . . . . . . 8 ((𝐹𝑀) ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ↔ ((𝐹𝑀) ∈ 𝐴 ∧ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅(𝐹𝑀)))
2221simprbi 499 . . . . . . 7 ((𝐹𝑀) ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} → ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅(𝐹𝑀))
2318, 22syl 17 . . . . . 6 ((𝜑𝑀 ∈ dom 𝑂) → ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅(𝐹𝑀))
245tfr1a 8022 . . . . . . . . 9 (Fun 𝐹 ∧ Lim dom 𝐹)
2524simpli 486 . . . . . . . 8 Fun 𝐹
26 funfn 6378 . . . . . . . 8 (Fun 𝐹𝐹 Fn dom 𝐹)
2725, 26mpbi 232 . . . . . . 7 𝐹 Fn dom 𝐹
2824simpri 488 . . . . . . . . 9 Lim dom 𝐹
29 limord 6243 . . . . . . . . 9 (Lim dom 𝐹 → Ord dom 𝐹)
3028, 29ax-mp 5 . . . . . . . 8 Ord dom 𝐹
31 inss2 4204 . . . . . . . . . 10 (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹
3213, 31eqsstrdi 4019 . . . . . . . . 9 (𝜑 → dom 𝑂 ⊆ dom 𝐹)
3332sselda 3965 . . . . . . . 8 ((𝜑𝑀 ∈ dom 𝑂) → 𝑀 ∈ dom 𝐹)
34 ordelss 6200 . . . . . . . 8 ((Ord dom 𝐹𝑀 ∈ dom 𝐹) → 𝑀 ⊆ dom 𝐹)
3530, 33, 34sylancr 589 . . . . . . 7 ((𝜑𝑀 ∈ dom 𝑂) → 𝑀 ⊆ dom 𝐹)
36 breq1 5060 . . . . . . . 8 (𝑗 = (𝐹𝑎) → (𝑗𝑅(𝐹𝑀) ↔ (𝐹𝑎)𝑅(𝐹𝑀)))
3736ralima 6992 . . . . . . 7 ((𝐹 Fn dom 𝐹𝑀 ⊆ dom 𝐹) → (∀𝑗 ∈ (𝐹𝑀)𝑗𝑅(𝐹𝑀) ↔ ∀𝑎𝑀 (𝐹𝑎)𝑅(𝐹𝑀)))
3827, 35, 37sylancr 589 . . . . . 6 ((𝜑𝑀 ∈ dom 𝑂) → (∀𝑗 ∈ (𝐹𝑀)𝑗𝑅(𝐹𝑀) ↔ ∀𝑎𝑀 (𝐹𝑎)𝑅(𝐹𝑀)))
3923, 38mpbid 234 . . . . 5 ((𝜑𝑀 ∈ dom 𝑂) → ∀𝑎𝑀 (𝐹𝑎)𝑅(𝐹𝑀))
4039adantrr 715 . . . 4 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → ∀𝑎𝑀 (𝐹𝑎)𝑅(𝐹𝑀))
41 simprr 771 . . . 4 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → 𝑁𝑀)
422, 40, 41rspcdva 3623 . . 3 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → (𝐹𝑁)𝑅(𝐹𝑀))
435, 6, 7, 8, 9, 10, 11ordtypelem1 8974 . . . . . 6 (𝜑𝑂 = (𝐹𝑇))
4443adantr 483 . . . . 5 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → 𝑂 = (𝐹𝑇))
4544fveq1d 6665 . . . 4 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → (𝑂𝑁) = ((𝐹𝑇)‘𝑁))
465, 6, 7, 8, 9, 10, 11ordtypelem2 8975 . . . . . . 7 (𝜑 → Ord 𝑇)
47 inss1 4203 . . . . . . . . . 10 (𝑇 ∩ dom 𝐹) ⊆ 𝑇
4813, 47eqsstrdi 4019 . . . . . . . . 9 (𝜑 → dom 𝑂𝑇)
4948sselda 3965 . . . . . . . 8 ((𝜑𝑀 ∈ dom 𝑂) → 𝑀𝑇)
5049adantrr 715 . . . . . . 7 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → 𝑀𝑇)
51 ordelss 6200 . . . . . . 7 ((Ord 𝑇𝑀𝑇) → 𝑀𝑇)
5246, 50, 51syl2an2r 683 . . . . . 6 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → 𝑀𝑇)
5352, 41sseldd 3966 . . . . 5 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → 𝑁𝑇)
5453fvresd 6683 . . . 4 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → ((𝐹𝑇)‘𝑁) = (𝐹𝑁))
5545, 54eqtrd 2854 . . 3 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → (𝑂𝑁) = (𝐹𝑁))
5644fveq1d 6665 . . . 4 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → (𝑂𝑀) = ((𝐹𝑇)‘𝑀))
5750fvresd 6683 . . . 4 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → ((𝐹𝑇)‘𝑀) = (𝐹𝑀))
5856, 57eqtrd 2854 . . 3 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → (𝑂𝑀) = (𝐹𝑀))
5942, 55, 583brtr4d 5089 . 2 ((𝜑 ∧ (𝑀 ∈ dom 𝑂𝑁𝑀)) → (𝑂𝑁)𝑅(𝑂𝑀))
6059expr 459 1 ((𝜑𝑀 ∈ dom 𝑂) → (𝑁𝑀 → (𝑂𝑁)𝑅(𝑂𝑀)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1530   ∈ wcel 2107  ∀wral 3136  ∃wrex 3137  {crab 3140  Vcvv 3493   ∩ cin 3933   ⊆ wss 3934   class class class wbr 5057   ↦ cmpt 5137   Se wse 5505   We wwe 5506  dom cdm 5548  ran crn 5549   ↾ cres 5550   “ cima 5551  Ord word 6183  Oncon0 6184  Lim wlim 6185  Fun wfun 6342   Fn wfn 6343  ‘cfv 6348  ℩crio 7105  recscrecs 7999  OrdIsocoi 8965 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-se 5508  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-wrecs 7939  df-recs 8000  df-oi 8966 This theorem is referenced by:  ordtypelem8  8981
 Copyright terms: Public domain W3C validator