Users' Mathboxes Mathbox for Stefan O'Rear < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  aomclem7 Structured version   Visualization version   GIF version

Theorem aomclem7 43050
Description: Lemma for dfac11 43052. (𝑅1𝐴) is well-orderable. (Contributed by Stefan O'Rear, 20-Jan-2015.)
Hypotheses
Ref Expression
aomclem6.b 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1 dom 𝑧)((𝑐𝑏 ∧ ¬ 𝑐𝑎) ∧ ∀𝑑 ∈ (𝑅1 dom 𝑧)(𝑑(𝑧 dom 𝑧)𝑐 → (𝑑𝑎𝑑𝑏)))}
aomclem6.c 𝐶 = (𝑎 ∈ V ↦ sup((𝑦𝑎), (𝑅1‘dom 𝑧), 𝐵))
aomclem6.d 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))
aomclem6.e 𝐸 = {⟨𝑎, 𝑏⟩ ∣ (𝐷 “ {𝑎}) ∈ (𝐷 “ {𝑏})}
aomclem6.f 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}
aomclem6.g 𝐺 = (if(dom 𝑧 = dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))
aomclem6.h 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))
aomclem6.a (𝜑𝐴 ∈ On)
aomclem6.y (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1𝐴)(𝑎 ≠ ∅ → (𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))
Assertion
Ref Expression
aomclem7 (𝜑 → ∃𝑏 𝑏 We (𝑅1𝐴))
Distinct variable groups:   𝑦,𝑧,𝑎,𝑏,𝑐,𝑑   𝜑,𝑎,𝑏,𝑐,𝑑,𝑧   𝐶,𝑎,𝑏,𝑐,𝑑   𝐷,𝑎,𝑏,𝑐,𝑑   𝐴,𝑎,𝑏,𝑐,𝑑,𝑧   𝐻,𝑎,𝑏,𝑐,𝑑,𝑧   𝐺,𝑑
Allowed substitution hints:   𝜑(𝑦)   𝐴(𝑦)   𝐵(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝐶(𝑦,𝑧)   𝐷(𝑦,𝑧)   𝐸(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝐹(𝑦,𝑧,𝑎,𝑏,𝑐,𝑑)   𝐺(𝑦,𝑧,𝑎,𝑏,𝑐)   𝐻(𝑦)

Proof of Theorem aomclem7
StepHypRef Expression
1 aomclem6.b . . 3 𝐵 = {⟨𝑎, 𝑏⟩ ∣ ∃𝑐 ∈ (𝑅1 dom 𝑧)((𝑐𝑏 ∧ ¬ 𝑐𝑎) ∧ ∀𝑑 ∈ (𝑅1 dom 𝑧)(𝑑(𝑧 dom 𝑧)𝑐 → (𝑑𝑎𝑑𝑏)))}
2 aomclem6.c . . 3 𝐶 = (𝑎 ∈ V ↦ sup((𝑦𝑎), (𝑅1‘dom 𝑧), 𝐵))
3 aomclem6.d . . 3 𝐷 = recs((𝑎 ∈ V ↦ (𝐶‘((𝑅1‘dom 𝑧) ∖ ran 𝑎))))
4 aomclem6.e . . 3 𝐸 = {⟨𝑎, 𝑏⟩ ∣ (𝐷 “ {𝑎}) ∈ (𝐷 “ {𝑏})}
5 aomclem6.f . . 3 𝐹 = {⟨𝑎, 𝑏⟩ ∣ ((rank‘𝑎) E (rank‘𝑏) ∨ ((rank‘𝑎) = (rank‘𝑏) ∧ 𝑎(𝑧‘suc (rank‘𝑎))𝑏))}
6 aomclem6.g . . 3 𝐺 = (if(dom 𝑧 = dom 𝑧, 𝐹, 𝐸) ∩ ((𝑅1‘dom 𝑧) × (𝑅1‘dom 𝑧)))
7 aomclem6.h . . 3 𝐻 = recs((𝑧 ∈ V ↦ 𝐺))
8 aomclem6.a . . 3 (𝜑𝐴 ∈ On)
9 aomclem6.y . . 3 (𝜑 → ∀𝑎 ∈ 𝒫 (𝑅1𝐴)(𝑎 ≠ ∅ → (𝑦𝑎) ∈ ((𝒫 𝑎 ∩ Fin) ∖ {∅})))
101, 2, 3, 4, 5, 6, 7, 8, 9aomclem6 43049 . 2 (𝜑 → (𝐻𝐴) We (𝑅1𝐴))
11 fvex 6917 . . 3 (𝐻𝐴) ∈ V
12 weeq1 5670 . . 3 (𝑏 = (𝐻𝐴) → (𝑏 We (𝑅1𝐴) ↔ (𝐻𝐴) We (𝑅1𝐴)))
1311, 12spcev 3605 . 2 ((𝐻𝐴) We (𝑅1𝐴) → ∃𝑏 𝑏 We (𝑅1𝐴))
1410, 13syl 17 1 (𝜑 → ∃𝑏 𝑏 We (𝑅1𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wex 1779  wcel 2108  wne 2939  wral 3060  wrex 3069  Vcvv 3479  cdif 3947  cin 3949  c0 4332  ifcif 4524  𝒫 cpw 4598  {csn 4624   cuni 4905   cint 4944   class class class wbr 5141  {copab 5203  cmpt 5223   E cep 5581   We wwe 5634   × cxp 5681  ccnv 5682  dom cdm 5683  ran crn 5684  cima 5686  Oncon0 6382  suc csuc 6384  cfv 6559  recscrecs 8406  Fincfn 8981  supcsup 9476  𝑅1cr1 9798  rankcrnk 9799
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-tp 4629  df-op 4631  df-uni 4906  df-int 4945  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5224  df-tr 5258  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5635  df-we 5637  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-pred 6319  df-ord 6385  df-on 6386  df-lim 6387  df-suc 6388  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-isom 6568  df-riota 7386  df-ov 7432  df-oprab 7433  df-mpo 7434  df-om 7884  df-1st 8010  df-2nd 8011  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-1o 8502  df-2o 8503  df-map 8864  df-en 8982  df-fin 8985  df-sup 9478  df-r1 9800  df-rank 9801
This theorem is referenced by:  aomclem8  43051
  Copyright terms: Public domain W3C validator