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

Theorem ordtypelem3 8308
 Description: Lemma for ordtype 8320. (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
ordtypelem3 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑀) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
Distinct variable groups:   𝑣,𝑢,𝐶   ,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧,𝑀   𝑅,,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧   𝐴,,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧   𝑡,𝑂,𝑢,𝑣,𝑥   𝜑,𝑡,𝑥   ,𝐹,𝑗,𝑡,𝑢,𝑣,𝑤,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑤,𝑣,𝑢,,𝑗)   𝐶(𝑥,𝑧,𝑤,𝑡,,𝑗)   𝑇(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,,𝑗)   𝐺(𝑥,𝑧,𝑤,𝑣,𝑢,𝑡,,𝑗)   𝑂(𝑧,𝑤,,𝑗)

Proof of Theorem ordtypelem3
StepHypRef Expression
1 inss2 3796 . . . . 5 (𝑇 ∩ dom 𝐹) ⊆ dom 𝐹
2 simpr 476 . . . . 5 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑀 ∈ (𝑇 ∩ dom 𝐹))
31, 2sseldi 3566 . . . 4 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑀 ∈ dom 𝐹)
4 ordtypelem.1 . . . . 5 𝐹 = recs(𝐺)
54tfr2a 7378 . . . 4 (𝑀 ∈ dom 𝐹 → (𝐹𝑀) = (𝐺‘(𝐹𝑀)))
63, 5syl 17 . . 3 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑀) = (𝐺‘(𝐹𝑀)))
74tfr1a 7377 . . . . . . . . 9 (Fun 𝐹 ∧ Lim dom 𝐹)
87simpri 477 . . . . . . . 8 Lim dom 𝐹
9 limord 5701 . . . . . . . 8 (Lim dom 𝐹 → Ord dom 𝐹)
108, 9ax-mp 5 . . . . . . 7 Ord dom 𝐹
11 ordelord 5662 . . . . . . 7 ((Ord dom 𝐹𝑀 ∈ dom 𝐹) → Ord 𝑀)
1210, 3, 11sylancr 694 . . . . . 6 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → Ord 𝑀)
134tfr2b 7379 . . . . . 6 (Ord 𝑀 → (𝑀 ∈ dom 𝐹 ↔ (𝐹𝑀) ∈ V))
1412, 13syl 17 . . . . 5 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝑀 ∈ dom 𝐹 ↔ (𝐹𝑀) ∈ V))
153, 14mpbid 221 . . . 4 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑀) ∈ V)
16 ordtypelem.2 . . . . . . 7 𝐶 = {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤}
17 rneq 5272 . . . . . . . . . 10 ( = (𝐹𝑀) → ran = ran (𝐹𝑀))
18 df-ima 5051 . . . . . . . . . 10 (𝐹𝑀) = ran (𝐹𝑀)
1917, 18syl6eqr 2662 . . . . . . . . 9 ( = (𝐹𝑀) → ran = (𝐹𝑀))
2019raleqdv 3121 . . . . . . . 8 ( = (𝐹𝑀) → (∀𝑗 ∈ ran 𝑗𝑅𝑤 ↔ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤))
2120rabbidv 3164 . . . . . . 7 ( = (𝐹𝑀) → {𝑤𝐴 ∣ ∀𝑗 ∈ ran 𝑗𝑅𝑤} = {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤})
2216, 21syl5eq 2656 . . . . . 6 ( = (𝐹𝑀) → 𝐶 = {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤})
2322raleqdv 3121 . . . . . 6 ( = (𝐹𝑀) → (∀𝑢𝐶 ¬ 𝑢𝑅𝑣 ↔ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
2422, 23riotaeqbidv 6514 . . . . 5 ( = (𝐹𝑀) → (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑅𝑣) = (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
25 ordtypelem.3 . . . . 5 𝐺 = ( ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑅𝑣))
26 riotaex 6515 . . . . 5 (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) ∈ V
2724, 25, 26fvmpt 6191 . . . 4 ((𝐹𝑀) ∈ V → (𝐺‘(𝐹𝑀)) = (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
2815, 27syl 17 . . 3 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐺‘(𝐹𝑀)) = (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
296, 28eqtrd 2644 . 2 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑀) = (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣))
30 ordtypelem.7 . . . . 5 (𝜑𝑅 We 𝐴)
3130adantr 480 . . . 4 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑅 We 𝐴)
32 ordtypelem.8 . . . . 5 (𝜑𝑅 Se 𝐴)
3332adantr 480 . . . 4 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑅 Se 𝐴)
34 ssrab2 3650 . . . . 5 {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ⊆ 𝐴
3534a1i 11 . . . 4 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ⊆ 𝐴)
36 inss1 3795 . . . . . . . 8 (𝑇 ∩ dom 𝐹) ⊆ 𝑇
3736, 2sseldi 3566 . . . . . . 7 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → 𝑀𝑇)
38 imaeq2 5381 . . . . . . . . . . 11 (𝑥 = 𝑀 → (𝐹𝑥) = (𝐹𝑀))
3938raleqdv 3121 . . . . . . . . . 10 (𝑥 = 𝑀 → (∀𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡 ↔ ∀𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑡))
4039rexbidv 3034 . . . . . . . . 9 (𝑥 = 𝑀 → (∃𝑡𝐴𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡 ↔ ∃𝑡𝐴𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑡))
41 ordtypelem.5 . . . . . . . . 9 𝑇 = {𝑥 ∈ On ∣ ∃𝑡𝐴𝑧 ∈ (𝐹𝑥)𝑧𝑅𝑡}
4240, 41elrab2 3333 . . . . . . . 8 (𝑀𝑇 ↔ (𝑀 ∈ On ∧ ∃𝑡𝐴𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑡))
4342simprbi 479 . . . . . . 7 (𝑀𝑇 → ∃𝑡𝐴𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑡)
4437, 43syl 17 . . . . . 6 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → ∃𝑡𝐴𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑡)
45 breq1 4586 . . . . . . . . 9 (𝑗 = 𝑧 → (𝑗𝑅𝑤𝑧𝑅𝑤))
4645cbvralv 3147 . . . . . . . 8 (∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤 ↔ ∀𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑤)
47 breq2 4587 . . . . . . . . 9 (𝑤 = 𝑡 → (𝑧𝑅𝑤𝑧𝑅𝑡))
4847ralbidv 2969 . . . . . . . 8 (𝑤 = 𝑡 → (∀𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑤 ↔ ∀𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑡))
4946, 48syl5bb 271 . . . . . . 7 (𝑤 = 𝑡 → (∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤 ↔ ∀𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑡))
5049cbvrexv 3148 . . . . . 6 (∃𝑤𝐴𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤 ↔ ∃𝑡𝐴𝑧 ∈ (𝐹𝑀)𝑧𝑅𝑡)
5144, 50sylibr 223 . . . . 5 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → ∃𝑤𝐴𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤)
52 rabn0 3912 . . . . 5 ({𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ≠ ∅ ↔ ∃𝑤𝐴𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤)
5351, 52sylibr 223 . . . 4 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ≠ ∅)
54 wereu2 5035 . . . 4 (((𝑅 We 𝐴𝑅 Se 𝐴) ∧ ({𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ⊆ 𝐴 ∧ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ≠ ∅)) → ∃!𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)
5531, 33, 35, 53, 54syl22anc 1319 . . 3 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → ∃!𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣)
56 riotacl2 6524 . . 3 (∃!𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣 → (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
5755, 56syl 17 . 2 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤}∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
5829, 57eqeltrd 2688 1 ((𝜑𝑀 ∈ (𝑇 ∩ dom 𝐹)) → (𝐹𝑀) ∈ {𝑣 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ∣ ∀𝑢 ∈ {𝑤𝐴 ∣ ∀𝑗 ∈ (𝐹𝑀)𝑗𝑅𝑤} ¬ 𝑢𝑅𝑣})
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  ∃!wreu 2898  {crab 2900  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   ↦ cmpt 4643   Se wse 4995   We wwe 4996  dom cdm 5038  ran crn 5039   ↾ cres 5040   “ cima 5041  Ord word 5639  Oncon0 5640  Lim wlim 5641  Fun wfun 5798  ‘cfv 5804  ℩crio 6510  recscrecs 7354  OrdIsocoi 8297 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-wrecs 7294  df-recs 7355 This theorem is referenced by:  ordtypelem4  8309  ordtypelem6  8311  ordtypelem7  8312
 Copyright terms: Public domain W3C validator