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

Theorem zorn2lem3 10141
Description: Lemma for zorn2 10149. (Contributed by NM, 3-Apr-1997.) (Revised by Mario Carneiro, 9-May-2015.)
Hypotheses
Ref Expression
zorn2lem.3 𝐹 = recs((𝑓 ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑤𝑣)))
zorn2lem.4 𝐶 = {𝑧𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧}
zorn2lem.5 𝐷 = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧}
Assertion
Ref Expression
zorn2lem3 ((𝑅 Po 𝐴 ∧ (𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅))) → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))
Distinct variable groups:   𝑓,𝑔,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧,𝐴   𝐷,𝑓,𝑢,𝑣,𝑦   𝑓,𝐹,𝑔,𝑢,𝑣,𝑥,𝑦,𝑧   𝑅,𝑓,𝑔,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧   𝑣,𝐶
Allowed substitution hints:   𝐶(𝑥,𝑦,𝑧,𝑤,𝑢,𝑓,𝑔)   𝐷(𝑥,𝑧,𝑤,𝑔)   𝐹(𝑤)

Proof of Theorem zorn2lem3
StepHypRef Expression
1 zorn2lem.3 . . . 4 𝐹 = recs((𝑓 ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑤𝑣)))
2 zorn2lem.4 . . . 4 𝐶 = {𝑧𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧}
3 zorn2lem.5 . . . 4 𝐷 = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧}
41, 2, 3zorn2lem2 10140 . . 3 ((𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅)) → (𝑦𝑥 → (𝐹𝑦)𝑅(𝐹𝑥)))
54adantl 485 . 2 ((𝑅 Po 𝐴 ∧ (𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅))) → (𝑦𝑥 → (𝐹𝑦)𝑅(𝐹𝑥)))
63ssrab3 4011 . . . 4 𝐷𝐴
71, 2, 3zorn2lem1 10139 . . . 4 ((𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅)) → (𝐹𝑥) ∈ 𝐷)
86, 7sselid 3915 . . 3 ((𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅)) → (𝐹𝑥) ∈ 𝐴)
9 breq1 5072 . . . . . 6 ((𝐹𝑥) = (𝐹𝑦) → ((𝐹𝑥)𝑅(𝐹𝑥) ↔ (𝐹𝑦)𝑅(𝐹𝑥)))
109biimprcd 253 . . . . 5 ((𝐹𝑦)𝑅(𝐹𝑥) → ((𝐹𝑥) = (𝐹𝑦) → (𝐹𝑥)𝑅(𝐹𝑥)))
11 poirr 5497 . . . . 5 ((𝑅 Po 𝐴 ∧ (𝐹𝑥) ∈ 𝐴) → ¬ (𝐹𝑥)𝑅(𝐹𝑥))
1210, 11nsyli 160 . . . 4 ((𝐹𝑦)𝑅(𝐹𝑥) → ((𝑅 Po 𝐴 ∧ (𝐹𝑥) ∈ 𝐴) → ¬ (𝐹𝑥) = (𝐹𝑦)))
1312com12 32 . . 3 ((𝑅 Po 𝐴 ∧ (𝐹𝑥) ∈ 𝐴) → ((𝐹𝑦)𝑅(𝐹𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)))
148, 13sylan2 596 . 2 ((𝑅 Po 𝐴 ∧ (𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅))) → ((𝐹𝑦)𝑅(𝐹𝑥) → ¬ (𝐹𝑥) = (𝐹𝑦)))
155, 14syld 47 1 ((𝑅 Po 𝐴 ∧ (𝑥 ∈ On ∧ (𝑤 We 𝐴𝐷 ≠ ∅))) → (𝑦𝑥 → ¬ (𝐹𝑥) = (𝐹𝑦)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 399   = wceq 1543  wcel 2112  wne 2943  wral 3064  {crab 3068  Vcvv 3423  c0 4253   class class class wbr 5069  cmpt 5151   Po wpo 5483   We wwe 5525  ran crn 5569  cima 5571  Oncon0 6233  cfv 6400  crio 7190  recscrecs 8130
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-rep 5195  ax-sep 5208  ax-nul 5215  ax-pr 5338  ax-un 7544
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4456  df-sn 4558  df-pr 4560  df-tp 4562  df-op 4564  df-uni 4836  df-iun 4922  df-br 5070  df-opab 5132  df-mpt 5152  df-tr 5178  df-id 5471  df-eprel 5477  df-po 5485  df-so 5486  df-fr 5526  df-we 5528  df-xp 5574  df-rel 5575  df-cnv 5576  df-co 5577  df-dm 5578  df-rn 5579  df-res 5580  df-ima 5581  df-pred 6178  df-ord 6236  df-on 6237  df-suc 6239  df-iota 6358  df-fun 6402  df-fn 6403  df-f 6404  df-f1 6405  df-fo 6406  df-f1o 6407  df-fv 6408  df-riota 7191  df-wrecs 8070  df-recs 8131
This theorem is referenced by:  zorn2lem4  10142
  Copyright terms: Public domain W3C validator