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

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

Proof of Theorem zorn2lem6
Dummy variables 𝑎 𝑏 𝑟 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poss 5186 . . . 4 ((𝐹𝑥) ⊆ 𝐴 → (𝑅 Po 𝐴𝑅 Po (𝐹𝑥)))
2 zorn2lem.3 . . . . 5 𝐹 = recs((𝑓 ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑤𝑣)))
3 zorn2lem.4 . . . . 5 𝐶 = {𝑧𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧}
4 zorn2lem.5 . . . . 5 𝐷 = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧}
5 zorn2lem.7 . . . . 5 𝐻 = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧}
62, 3, 4, 5zorn2lem5 9545 . . . 4 (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (𝐹𝑥) ⊆ 𝐴)
71, 6syl11 33 . . 3 (𝑅 Po 𝐴 → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → 𝑅 Po (𝐹𝑥)))
82tfr1 7667 . . . . . . . 8 𝐹 Fn On
9 fnfun 6139 . . . . . . . 8 (𝐹 Fn On → Fun 𝐹)
10 fvelima 6407 . . . . . . . . . . 11 ((Fun 𝐹𝑠 ∈ (𝐹𝑥)) → ∃𝑏𝑥 (𝐹𝑏) = 𝑠)
11 df-rex 3070 . . . . . . . . . . 11 (∃𝑏𝑥 (𝐹𝑏) = 𝑠 ↔ ∃𝑏(𝑏𝑥 ∧ (𝐹𝑏) = 𝑠))
1210, 11sylib 209 . . . . . . . . . 10 ((Fun 𝐹𝑠 ∈ (𝐹𝑥)) → ∃𝑏(𝑏𝑥 ∧ (𝐹𝑏) = 𝑠))
1312ex 398 . . . . . . . . 9 (Fun 𝐹 → (𝑠 ∈ (𝐹𝑥) → ∃𝑏(𝑏𝑥 ∧ (𝐹𝑏) = 𝑠)))
14 fvelima 6407 . . . . . . . . . . 11 ((Fun 𝐹𝑟 ∈ (𝐹𝑥)) → ∃𝑎𝑥 (𝐹𝑎) = 𝑟)
15 df-rex 3070 . . . . . . . . . . 11 (∃𝑎𝑥 (𝐹𝑎) = 𝑟 ↔ ∃𝑎(𝑎𝑥 ∧ (𝐹𝑎) = 𝑟))
1614, 15sylib 209 . . . . . . . . . 10 ((Fun 𝐹𝑟 ∈ (𝐹𝑥)) → ∃𝑎(𝑎𝑥 ∧ (𝐹𝑎) = 𝑟))
1716ex 398 . . . . . . . . 9 (Fun 𝐹 → (𝑟 ∈ (𝐹𝑥) → ∃𝑎(𝑎𝑥 ∧ (𝐹𝑎) = 𝑟)))
1813, 17anim12d 597 . . . . . . . 8 (Fun 𝐹 → ((𝑠 ∈ (𝐹𝑥) ∧ 𝑟 ∈ (𝐹𝑥)) → (∃𝑏(𝑏𝑥 ∧ (𝐹𝑏) = 𝑠) ∧ ∃𝑎(𝑎𝑥 ∧ (𝐹𝑎) = 𝑟))))
198, 9, 18mp2b 10 . . . . . . 7 ((𝑠 ∈ (𝐹𝑥) ∧ 𝑟 ∈ (𝐹𝑥)) → (∃𝑏(𝑏𝑥 ∧ (𝐹𝑏) = 𝑠) ∧ ∃𝑎(𝑎𝑥 ∧ (𝐹𝑎) = 𝑟)))
20 an4 636 . . . . . . . . 9 (((𝑏𝑥𝑎𝑥) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) ↔ ((𝑏𝑥 ∧ (𝐹𝑏) = 𝑠) ∧ (𝑎𝑥 ∧ (𝐹𝑎) = 𝑟)))
21202exbii 1928 . . . . . . . 8 (∃𝑏𝑎((𝑏𝑥𝑎𝑥) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) ↔ ∃𝑏𝑎((𝑏𝑥 ∧ (𝐹𝑏) = 𝑠) ∧ (𝑎𝑥 ∧ (𝐹𝑎) = 𝑟)))
22 eeanv 2347 . . . . . . . 8 (∃𝑏𝑎((𝑏𝑥 ∧ (𝐹𝑏) = 𝑠) ∧ (𝑎𝑥 ∧ (𝐹𝑎) = 𝑟)) ↔ (∃𝑏(𝑏𝑥 ∧ (𝐹𝑏) = 𝑠) ∧ ∃𝑎(𝑎𝑥 ∧ (𝐹𝑎) = 𝑟)))
2321, 22bitri 265 . . . . . . 7 (∃𝑏𝑎((𝑏𝑥𝑎𝑥) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) ↔ (∃𝑏(𝑏𝑥 ∧ (𝐹𝑏) = 𝑠) ∧ ∃𝑎(𝑎𝑥 ∧ (𝐹𝑎) = 𝑟)))
2419, 23sylibr 225 . . . . . 6 ((𝑠 ∈ (𝐹𝑥) ∧ 𝑟 ∈ (𝐹𝑥)) → ∃𝑏𝑎((𝑏𝑥𝑎𝑥) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)))
255neeq1i 3010 . . . . . . . . . . 11 (𝐻 ≠ ∅ ↔ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧} ≠ ∅)
2625ralbii 3132 . . . . . . . . . 10 (∀𝑦𝑥 𝐻 ≠ ∅ ↔ ∀𝑦𝑥 {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧} ≠ ∅)
27 imaeq2 5613 . . . . . . . . . . . . . . 15 (𝑦 = 𝑏 → (𝐹𝑦) = (𝐹𝑏))
2827raleqdv 3297 . . . . . . . . . . . . . 14 (𝑦 = 𝑏 → (∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧 ↔ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧))
2928rabbidv 3343 . . . . . . . . . . . . 13 (𝑦 = 𝑏 → {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧} = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧})
3029neeq1d 3005 . . . . . . . . . . . 12 (𝑦 = 𝑏 → ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧} ≠ ∅ ↔ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅))
3130rspccv 3462 . . . . . . . . . . 11 (∀𝑦𝑥 {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧} ≠ ∅ → (𝑏𝑥 → {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅))
32 imaeq2 5613 . . . . . . . . . . . . . . 15 (𝑦 = 𝑎 → (𝐹𝑦) = (𝐹𝑎))
3332raleqdv 3297 . . . . . . . . . . . . . 14 (𝑦 = 𝑎 → (∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧 ↔ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧))
3433rabbidv 3343 . . . . . . . . . . . . 13 (𝑦 = 𝑎 → {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧} = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧})
3534neeq1d 3005 . . . . . . . . . . . 12 (𝑦 = 𝑎 → ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧} ≠ ∅ ↔ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅))
3635rspccv 3462 . . . . . . . . . . 11 (∀𝑦𝑥 {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧} ≠ ∅ → (𝑎𝑥 → {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅))
3731, 36anim12d 597 . . . . . . . . . 10 (∀𝑦𝑥 {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧} ≠ ∅ → ((𝑏𝑥𝑎𝑥) → ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)))
3826, 37sylbi 208 . . . . . . . . 9 (∀𝑦𝑥 𝐻 ≠ ∅ → ((𝑏𝑥𝑎𝑥) → ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)))
39 onelon 5902 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝑏𝑥) → 𝑏 ∈ On)
40 onelon 5902 . . . . . . . . . . . . . . . 16 ((𝑥 ∈ On ∧ 𝑎𝑥) → 𝑎 ∈ On)
4139, 40anim12dan 606 . . . . . . . . . . . . . . 15 ((𝑥 ∈ On ∧ (𝑏𝑥𝑎𝑥)) → (𝑏 ∈ On ∧ 𝑎 ∈ On))
4241ex 398 . . . . . . . . . . . . . 14 (𝑥 ∈ On → ((𝑏𝑥𝑎𝑥) → (𝑏 ∈ On ∧ 𝑎 ∈ On)))
43 eloni 5887 . . . . . . . . . . . . . . . . . 18 (𝑏 ∈ On → Ord 𝑏)
44 eloni 5887 . . . . . . . . . . . . . . . . . 18 (𝑎 ∈ On → Ord 𝑎)
45 ordtri3or 5909 . . . . . . . . . . . . . . . . . 18 ((Ord 𝑏 ∧ Ord 𝑎) → (𝑏𝑎𝑏 = 𝑎𝑎𝑏))
4643, 44, 45syl2an 584 . . . . . . . . . . . . . . . . 17 ((𝑏 ∈ On ∧ 𝑎 ∈ On) → (𝑏𝑎𝑏 = 𝑎𝑎𝑏))
47 eqid 2774 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧}
482, 3, 47zorn2lem2 9542 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎 ∈ On ∧ (𝑤 We 𝐴 ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)) → (𝑏𝑎 → (𝐹𝑏)𝑅(𝐹𝑎)))
4948adantll 694 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)) → (𝑏𝑎 → (𝐹𝑏)𝑅(𝐹𝑎)))
50 breq12 4802 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → ((𝐹𝑏)𝑅(𝐹𝑎) ↔ 𝑠𝑅𝑟))
5150biimpcd 240 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑏)𝑅(𝐹𝑎) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → 𝑠𝑅𝑟))
5249, 51syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)) → (𝑏𝑎 → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → 𝑠𝑅𝑟)))
5352com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑏𝑎𝑠𝑅𝑟)))
5453adantrrl 704 . . . . . . . . . . . . . . . . . . 19 (((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅))) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑏𝑎𝑠𝑅𝑟)))
5554imp 394 . . . . . . . . . . . . . . . . . 18 ((((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅))) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) → (𝑏𝑎𝑠𝑅𝑟))
56 fveq2 6348 . . . . . . . . . . . . . . . . . . . 20 (𝑏 = 𝑎 → (𝐹𝑏) = (𝐹𝑎))
57 eqeq12 2787 . . . . . . . . . . . . . . . . . . . 20 (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → ((𝐹𝑏) = (𝐹𝑎) ↔ 𝑠 = 𝑟))
5856, 57syl5ib 235 . . . . . . . . . . . . . . . . . . 19 (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑏 = 𝑎𝑠 = 𝑟))
5958adantl 468 . . . . . . . . . . . . . . . . . 18 ((((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅))) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) → (𝑏 = 𝑎𝑠 = 𝑟))
60 eqid 2774 . . . . . . . . . . . . . . . . . . . . . . . 24 {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧}
612, 3, 60zorn2lem2 9542 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏 ∈ On ∧ (𝑤 We 𝐴 ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅)) → (𝑎𝑏 → (𝐹𝑎)𝑅(𝐹𝑏)))
6261adantlr 695 . . . . . . . . . . . . . . . . . . . . . 22 (((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅)) → (𝑎𝑏 → (𝐹𝑎)𝑅(𝐹𝑏)))
63 breq12 4802 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝐹𝑎) = 𝑟 ∧ (𝐹𝑏) = 𝑠) → ((𝐹𝑎)𝑅(𝐹𝑏) ↔ 𝑟𝑅𝑠))
6463ancoms 447 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → ((𝐹𝑎)𝑅(𝐹𝑏) ↔ 𝑟𝑅𝑠))
6564biimpcd 240 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐹𝑎)𝑅(𝐹𝑏) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → 𝑟𝑅𝑠))
6662, 65syl6 35 . . . . . . . . . . . . . . . . . . . . 21 (((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅)) → (𝑎𝑏 → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → 𝑟𝑅𝑠)))
6766com23 86 . . . . . . . . . . . . . . . . . . . 20 (((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅)) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑎𝑏𝑟𝑅𝑠)))
6867adantrrr 705 . . . . . . . . . . . . . . . . . . 19 (((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅))) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑎𝑏𝑟𝑅𝑠)))
6968imp 394 . . . . . . . . . . . . . . . . . 18 ((((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅))) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) → (𝑎𝑏𝑟𝑅𝑠))
7055, 59, 693orim123d 1558 . . . . . . . . . . . . . . . . 17 ((((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅))) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) → ((𝑏𝑎𝑏 = 𝑎𝑎𝑏) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))
7146, 70syl5 34 . . . . . . . . . . . . . . . 16 ((((𝑏 ∈ On ∧ 𝑎 ∈ On) ∧ (𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅))) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) → ((𝑏 ∈ On ∧ 𝑎 ∈ On) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))
7271exp31 407 . . . . . . . . . . . . . . 15 ((𝑏 ∈ On ∧ 𝑎 ∈ On) → ((𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → ((𝑏 ∈ On ∧ 𝑎 ∈ On) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))))
7372com4r 94 . . . . . . . . . . . . . 14 ((𝑏 ∈ On ∧ 𝑎 ∈ On) → ((𝑏 ∈ On ∧ 𝑎 ∈ On) → ((𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))))
7442, 42, 73syl6c 70 . . . . . . . . . . . . 13 (𝑥 ∈ On → ((𝑏𝑥𝑎𝑥) → ((𝑤 We 𝐴 ∧ ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))))
7574exp4a 419 . . . . . . . . . . . 12 (𝑥 ∈ On → ((𝑏𝑥𝑎𝑥) → (𝑤 We 𝐴 → (({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠))))))
7675com3r 87 . . . . . . . . . . 11 (𝑤 We 𝐴 → (𝑥 ∈ On → ((𝑏𝑥𝑎𝑥) → (({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠))))))
7776imp 394 . . . . . . . . . 10 ((𝑤 We 𝐴𝑥 ∈ On) → ((𝑏𝑥𝑎𝑥) → (({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))))
7877a2d 29 . . . . . . . . 9 ((𝑤 We 𝐴𝑥 ∈ On) → (((𝑏𝑥𝑎𝑥) → ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑏)𝑔𝑅𝑧} ≠ ∅ ∧ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑎)𝑔𝑅𝑧} ≠ ∅)) → ((𝑏𝑥𝑎𝑥) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))))
7938, 78syl5 34 . . . . . . . 8 ((𝑤 We 𝐴𝑥 ∈ On) → (∀𝑦𝑥 𝐻 ≠ ∅ → ((𝑏𝑥𝑎𝑥) → (((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))))
8079imp4b 409 . . . . . . 7 (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (((𝑏𝑥𝑎𝑥) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))
8180exlimdvv 2017 . . . . . 6 (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (∃𝑏𝑎((𝑏𝑥𝑎𝑥) ∧ ((𝐹𝑏) = 𝑠 ∧ (𝐹𝑎) = 𝑟)) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))
8224, 81syl5 34 . . . . 5 (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → ((𝑠 ∈ (𝐹𝑥) ∧ 𝑟 ∈ (𝐹𝑥)) → (𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))
8382ralrimivv 3122 . . . 4 (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → ∀𝑠 ∈ (𝐹𝑥)∀𝑟 ∈ (𝐹𝑥)(𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠))
8483a1i 11 . . 3 (𝑅 Po 𝐴 → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → ∀𝑠 ∈ (𝐹𝑥)∀𝑟 ∈ (𝐹𝑥)(𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))
857, 84jcad 503 . 2 (𝑅 Po 𝐴 → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (𝑅 Po (𝐹𝑥) ∧ ∀𝑠 ∈ (𝐹𝑥)∀𝑟 ∈ (𝐹𝑥)(𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠))))
86 df-so 5185 . 2 (𝑅 Or (𝐹𝑥) ↔ (𝑅 Po (𝐹𝑥) ∧ ∀𝑠 ∈ (𝐹𝑥)∀𝑟 ∈ (𝐹𝑥)(𝑠𝑅𝑟𝑠 = 𝑟𝑟𝑅𝑠)))
8785, 86syl6ibr 243 1 (𝑅 Po 𝐴 → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → 𝑅 Or (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 383  w3o 1097   = wceq 1634  wex 1855  wcel 2148  wne 2946  wral 3064  wrex 3065  {crab 3068  Vcvv 3355  wss 3729  c0 4073   class class class wbr 4797  cmpt 4876   Po wpo 5182   Or wor 5183   We wwe 5221  ran crn 5264  cima 5266  Ord word 5876  Oncon0 5877  Fun wfun 6036   Fn wfn 6037  cfv 6042  crio 6772  recscrecs 7641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-8 2150  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-rep 4917  ax-sep 4928  ax-nul 4936  ax-pow 4988  ax-pr 5048  ax-un 7117
This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3or 1099  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-ne 2947  df-ral 3069  df-rex 3070  df-reu 3071  df-rmo 3072  df-rab 3073  df-v 3357  df-sbc 3594  df-csb 3689  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-pss 3745  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-tp 4331  df-op 4333  df-uni 4586  df-iun 4667  df-br 4798  df-opab 4860  df-mpt 4877  df-tr 4900  df-id 5171  df-eprel 5176  df-po 5184  df-so 5185  df-fr 5222  df-we 5224  df-xp 5269  df-rel 5270  df-cnv 5271  df-co 5272  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276  df-pred 5834  df-ord 5880  df-on 5881  df-suc 5883  df-iota 6005  df-fun 6044  df-fn 6045  df-f 6046  df-f1 6047  df-fo 6048  df-f1o 6049  df-fv 6050  df-riota 6773  df-wrecs 7580  df-recs 7642
This theorem is referenced by:  zorn2lem7  9547
  Copyright terms: Public domain W3C validator