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

Theorem zorn2lem7 9918
Description: Lemma for zorn2 9922. (Contributed by NM, 6-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
zorn2lem7 ((𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏)
Distinct variable groups:   𝑎,𝑏,𝑓,𝑔,𝑟,𝑠,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧,𝐴   𝐷,𝑎,𝑏,𝑓,𝑢,𝑣,𝑦   𝐹,𝑎,𝑏,𝑓,𝑔,𝑟,𝑠,𝑢,𝑣,𝑥,𝑦,𝑧   𝑅,𝑎,𝑏,𝑓,𝑔,𝑟,𝑠,𝑢,𝑣,𝑤,𝑥,𝑦,𝑧   𝑣,𝐶   𝑥,𝐻,𝑢,𝑣,𝑓,𝑠,𝑟,𝑎,𝑏
Allowed substitution hints:   𝐶(𝑥,𝑦,𝑧,𝑤,𝑢,𝑓,𝑔,𝑠,𝑟,𝑎,𝑏)   𝐷(𝑥,𝑧,𝑤,𝑔,𝑠,𝑟)   𝐹(𝑤)   𝐻(𝑦,𝑧,𝑤,𝑔)

Proof of Theorem zorn2lem7
StepHypRef Expression
1 ween 9455 . . 3 (𝐴 ∈ dom card ↔ ∃𝑤 𝑤 We 𝐴)
2 zorn2lem.3 . . . . . . . . 9 𝐹 = recs((𝑓 ∈ V ↦ (𝑣𝐶𝑢𝐶 ¬ 𝑢𝑤𝑣)))
3 zorn2lem.4 . . . . . . . . 9 𝐶 = {𝑧𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧}
4 zorn2lem.5 . . . . . . . . 9 𝐷 = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧}
52, 3, 4zorn2lem4 9915 . . . . . . . 8 ((𝑅 Po 𝐴𝑤 We 𝐴) → ∃𝑥 ∈ On 𝐷 = ∅)
6 imaeq2 5924 . . . . . . . . . . . . . 14 (𝑥 = 𝑦 → (𝐹𝑥) = (𝐹𝑦))
76raleqdv 3421 . . . . . . . . . . . . 13 (𝑥 = 𝑦 → (∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧 ↔ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧))
87rabbidv 3486 . . . . . . . . . . . 12 (𝑥 = 𝑦 → {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧} = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧})
9 zorn2lem.7 . . . . . . . . . . . 12 𝐻 = {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑦)𝑔𝑅𝑧}
108, 4, 93eqtr4g 2886 . . . . . . . . . . 11 (𝑥 = 𝑦𝐷 = 𝐻)
1110eqeq1d 2828 . . . . . . . . . 10 (𝑥 = 𝑦 → (𝐷 = ∅ ↔ 𝐻 = ∅))
1211onminex 7515 . . . . . . . . 9 (∃𝑥 ∈ On 𝐷 = ∅ → ∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦𝑥 ¬ 𝐻 = ∅))
13 df-ne 3022 . . . . . . . . . . . 12 (𝐻 ≠ ∅ ↔ ¬ 𝐻 = ∅)
1413ralbii 3170 . . . . . . . . . . 11 (∀𝑦𝑥 𝐻 ≠ ∅ ↔ ∀𝑦𝑥 ¬ 𝐻 = ∅)
1514anbi2i 622 . . . . . . . . . 10 ((𝐷 = ∅ ∧ ∀𝑦𝑥 𝐻 ≠ ∅) ↔ (𝐷 = ∅ ∧ ∀𝑦𝑥 ¬ 𝐻 = ∅))
1615rexbii 3252 . . . . . . . . 9 (∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦𝑥 𝐻 ≠ ∅) ↔ ∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦𝑥 ¬ 𝐻 = ∅))
1712, 16sylibr 235 . . . . . . . 8 (∃𝑥 ∈ On 𝐷 = ∅ → ∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦𝑥 𝐻 ≠ ∅))
182, 3, 4, 9zorn2lem5 9916 . . . . . . . . . . . . . . . . . . . 20 (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (𝐹𝑥) ⊆ 𝐴)
1918a1i 11 . . . . . . . . . . . . . . . . . . 19 (𝑅 Po 𝐴 → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (𝐹𝑥) ⊆ 𝐴))
202, 3, 4, 9zorn2lem6 9917 . . . . . . . . . . . . . . . . . . 19 (𝑅 Po 𝐴 → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → 𝑅 Or (𝐹𝑥)))
2119, 20jcad 513 . . . . . . . . . . . . . . . . . 18 (𝑅 Po 𝐴 → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → ((𝐹𝑥) ⊆ 𝐴𝑅 Or (𝐹𝑥))))
222tfr1 8029 . . . . . . . . . . . . . . . . . . . 20 𝐹 Fn On
23 fnfun 6452 . . . . . . . . . . . . . . . . . . . 20 (𝐹 Fn On → Fun 𝐹)
24 vex 3503 . . . . . . . . . . . . . . . . . . . . 21 𝑥 ∈ V
2524funimaex 6440 . . . . . . . . . . . . . . . . . . . 20 (Fun 𝐹 → (𝐹𝑥) ∈ V)
2622, 23, 25mp2b 10 . . . . . . . . . . . . . . . . . . 19 (𝐹𝑥) ∈ V
27 sseq1 3996 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑥) → (𝑠𝐴 ↔ (𝐹𝑥) ⊆ 𝐴))
28 soeq2 5494 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑥) → (𝑅 Or 𝑠𝑅 Or (𝐹𝑥)))
2927, 28anbi12d 630 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝐹𝑥) → ((𝑠𝐴𝑅 Or 𝑠) ↔ ((𝐹𝑥) ⊆ 𝐴𝑅 Or (𝐹𝑥))))
30 raleq 3411 . . . . . . . . . . . . . . . . . . . . 21 (𝑠 = (𝐹𝑥) → (∀𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎) ↔ ∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎)))
3130rexbidv 3302 . . . . . . . . . . . . . . . . . . . 20 (𝑠 = (𝐹𝑥) → (∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎) ↔ ∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎)))
3229, 31imbi12d 346 . . . . . . . . . . . . . . . . . . 19 (𝑠 = (𝐹𝑥) → (((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎)) ↔ (((𝐹𝑥) ⊆ 𝐴𝑅 Or (𝐹𝑥)) → ∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎))))
3326, 32spcv 3610 . . . . . . . . . . . . . . . . . 18 (∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎)) → (((𝐹𝑥) ⊆ 𝐴𝑅 Or (𝐹𝑥)) → ∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎)))
3421, 33sylan9 508 . . . . . . . . . . . . . . . . 17 ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → ∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎)))
3534adantld 491 . . . . . . . . . . . . . . . 16 ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → ((𝐷 = ∅ ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → ∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎)))
3635imp 407 . . . . . . . . . . . . . . 15 (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ (𝐷 = ∅ ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅))) → ∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎))
37 noel 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ¬ 𝑏 ∈ ∅
3818sseld 3970 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (𝑟 ∈ (𝐹𝑥) → 𝑟𝐴))
39 3anass 1089 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑟𝐴𝑎𝐴𝑏𝐴) ↔ (𝑟𝐴 ∧ (𝑎𝐴𝑏𝐴)))
40 potr 5485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 ((𝑅 Po 𝐴 ∧ (𝑟𝐴𝑎𝐴𝑏𝐴)) → ((𝑟𝑅𝑎𝑎𝑅𝑏) → 𝑟𝑅𝑏))
4139, 40sylan2br 594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 ((𝑅 Po 𝐴 ∧ (𝑟𝐴 ∧ (𝑎𝐴𝑏𝐴))) → ((𝑟𝑅𝑎𝑎𝑅𝑏) → 𝑟𝑅𝑏))
4241expcomd 417 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 ((𝑅 Po 𝐴 ∧ (𝑟𝐴 ∧ (𝑎𝐴𝑏𝐴))) → (𝑎𝑅𝑏 → (𝑟𝑅𝑎𝑟𝑅𝑏)))
4342imp 407 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑅 Po 𝐴 ∧ (𝑟𝐴 ∧ (𝑎𝐴𝑏𝐴))) ∧ 𝑎𝑅𝑏) → (𝑟𝑅𝑎𝑟𝑅𝑏))
44 breq1 5066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46 (𝑟 = 𝑎 → (𝑟𝑅𝑏𝑎𝑅𝑏))
4544biimprcd 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 (𝑎𝑅𝑏 → (𝑟 = 𝑎𝑟𝑅𝑏))
4645adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44 (((𝑅 Po 𝐴 ∧ (𝑟𝐴 ∧ (𝑎𝐴𝑏𝐴))) ∧ 𝑎𝑅𝑏) → (𝑟 = 𝑎𝑟𝑅𝑏))
4743, 46jaod 855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43 (((𝑅 Po 𝐴 ∧ (𝑟𝐴 ∧ (𝑎𝐴𝑏𝐴))) ∧ 𝑎𝑅𝑏) → ((𝑟𝑅𝑎𝑟 = 𝑎) → 𝑟𝑅𝑏))
4847exp42 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑅 Po 𝐴 → (𝑟𝐴 → ((𝑎𝐴𝑏𝐴) → (𝑎𝑅𝑏 → ((𝑟𝑅𝑎𝑟 = 𝑎) → 𝑟𝑅𝑏)))))
4938, 48sylan9r 509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → (𝑟 ∈ (𝐹𝑥) → ((𝑎𝐴𝑏𝐴) → (𝑎𝑅𝑏 → ((𝑟𝑅𝑎𝑟 = 𝑎) → 𝑟𝑅𝑏)))))
5049com24 95 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → (𝑎𝑅𝑏 → ((𝑎𝐴𝑏𝐴) → (𝑟 ∈ (𝐹𝑥) → ((𝑟𝑅𝑎𝑟 = 𝑎) → 𝑟𝑅𝑏)))))
5150com23 86 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → ((𝑎𝐴𝑏𝐴) → (𝑎𝑅𝑏 → (𝑟 ∈ (𝐹𝑥) → ((𝑟𝑅𝑎𝑟 = 𝑎) → 𝑟𝑅𝑏)))))
5251imp31 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 ((((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑎𝑅𝑏) → (𝑟 ∈ (𝐹𝑥) → ((𝑟𝑅𝑎𝑟 = 𝑎) → 𝑟𝑅𝑏)))
5352a2d 29 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑎𝑅𝑏) → ((𝑟 ∈ (𝐹𝑥) → (𝑟𝑅𝑎𝑟 = 𝑎)) → (𝑟 ∈ (𝐹𝑥) → 𝑟𝑅𝑏)))
5453ralimdv2 3181 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑎𝑅𝑏) → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ∀𝑟 ∈ (𝐹𝑥)𝑟𝑅𝑏))
55 breq1 5066 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝑟 = 𝑔 → (𝑟𝑅𝑏𝑔𝑅𝑏))
5655cbvralvw 3455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 (∀𝑟 ∈ (𝐹𝑥)𝑟𝑅𝑏 ↔ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑏)
57 breq2 5067 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 (𝑧 = 𝑏 → (𝑔𝑅𝑧𝑔𝑅𝑏))
5857ralbidv 3202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝑧 = 𝑏 → (∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧 ↔ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑏))
5958elrab 3684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝑏 ∈ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧} ↔ (𝑏𝐴 ∧ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑏))
604eqeq1i 2831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 (𝐷 = ∅ ↔ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧} = ∅)
61 eleq2 2906 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 ({𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧} = ∅ → (𝑏 ∈ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧} ↔ 𝑏 ∈ ∅))
6260, 61sylbi 218 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 (𝐷 = ∅ → (𝑏 ∈ {𝑧𝐴 ∣ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑧} ↔ 𝑏 ∈ ∅))
6359, 62syl5bbr 286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 (𝐷 = ∅ → ((𝑏𝐴 ∧ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑏) ↔ 𝑏 ∈ ∅))
6463biimpd 230 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 (𝐷 = ∅ → ((𝑏𝐴 ∧ ∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑏) → 𝑏 ∈ ∅))
6564expdimp 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 ((𝐷 = ∅ ∧ 𝑏𝐴) → (∀𝑔 ∈ (𝐹𝑥)𝑔𝑅𝑏𝑏 ∈ ∅))
6656, 65syl5bi 243 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 ((𝐷 = ∅ ∧ 𝑏𝐴) → (∀𝑟 ∈ (𝐹𝑥)𝑟𝑅𝑏𝑏 ∈ ∅))
6754, 66sylan9r 509 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (((𝐷 = ∅ ∧ 𝑏𝐴) ∧ (((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) ∧ (𝑎𝐴𝑏𝐴)) ∧ 𝑎𝑅𝑏)) → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → 𝑏 ∈ ∅))
6867exp32 421 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((𝐷 = ∅ ∧ 𝑏𝐴) → (((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) ∧ (𝑎𝐴𝑏𝐴)) → (𝑎𝑅𝑏 → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → 𝑏 ∈ ∅))))
6968com34 91 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((𝐷 = ∅ ∧ 𝑏𝐴) → (((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) ∧ (𝑎𝐴𝑏𝐴)) → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → (𝑎𝑅𝑏𝑏 ∈ ∅))))
7069imp31 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((((𝐷 = ∅ ∧ 𝑏𝐴) ∧ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) ∧ (𝑎𝐴𝑏𝐴))) ∧ ∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎)) → (𝑎𝑅𝑏𝑏 ∈ ∅))
7137, 70mtoi 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((((𝐷 = ∅ ∧ 𝑏𝐴) ∧ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) ∧ (𝑎𝐴𝑏𝐴))) ∧ ∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎)) → ¬ 𝑎𝑅𝑏)
7271exp42 436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ((𝐷 = ∅ ∧ 𝑏𝐴) → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → ((𝑎𝐴𝑏𝐴) → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))
7372exp4a 432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((𝐷 = ∅ ∧ 𝑏𝐴) → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → (𝑎𝐴 → (𝑏𝐴 → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))))
7473com34 91 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((𝐷 = ∅ ∧ 𝑏𝐴) → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → (𝑏𝐴 → (𝑎𝐴 → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))))
7574ex 413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝐷 = ∅ → (𝑏𝐴 → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → (𝑏𝐴 → (𝑎𝐴 → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))))
7675com4r 94 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑏𝐴 → (𝐷 = ∅ → (𝑏𝐴 → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → (𝑎𝐴 → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))))
7776pm2.43a 54 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑏𝐴 → (𝐷 = ∅ → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅)) → (𝑎𝐴 → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))))
7877impd 411 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏𝐴 → ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅))) → (𝑎𝐴 → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))
7978com4l 92 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅))) → (𝑎𝐴 → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → (𝑏𝐴 → ¬ 𝑎𝑅𝑏))))
8079impd 411 . . . . . . . . . . . . . . . . . . . . . 22 ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅))) → ((𝑎𝐴 ∧ ∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎)) → (𝑏𝐴 → ¬ 𝑎𝑅𝑏)))
8180ralrimdv 3193 . . . . . . . . . . . . . . . . . . . . 21 ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅))) → ((𝑎𝐴 ∧ ∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎)) → ∀𝑏𝐴 ¬ 𝑎𝑅𝑏))
8281expd 416 . . . . . . . . . . . . . . . . . . . 20 ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅))) → (𝑎𝐴 → (∀𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ∀𝑏𝐴 ¬ 𝑎𝑅𝑏)))
8382reximdvai 3277 . . . . . . . . . . . . . . . . . . 19 ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅))) → (∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))
8483exp32 421 . . . . . . . . . . . . . . . . . 18 (𝐷 = ∅ → (𝑅 Po 𝐴 → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))))
8584com12 32 . . . . . . . . . . . . . . . . 17 (𝑅 Po 𝐴 → (𝐷 = ∅ → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))))
8685adantr 481 . . . . . . . . . . . . . . . 16 ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → (𝐷 = ∅ → (((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))))
8786imp32 419 . . . . . . . . . . . . . . 15 (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ (𝐷 = ∅ ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅))) → (∃𝑎𝐴𝑟 ∈ (𝐹𝑥)(𝑟𝑅𝑎𝑟 = 𝑎) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))
8836, 87mpd 15 . . . . . . . . . . . . . 14 (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ (𝐷 = ∅ ∧ ((𝑤 We 𝐴𝑥 ∈ On) ∧ ∀𝑦𝑥 𝐻 ≠ ∅))) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏)
8988exp45 439 . . . . . . . . . . . . 13 ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → (𝐷 = ∅ → ((𝑤 We 𝐴𝑥 ∈ On) → (∀𝑦𝑥 𝐻 ≠ ∅ → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))))
9089com23 86 . . . . . . . . . . . 12 ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → ((𝑤 We 𝐴𝑥 ∈ On) → (𝐷 = ∅ → (∀𝑦𝑥 𝐻 ≠ ∅ → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))))
9190expdimp 453 . . . . . . . . . . 11 (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → (𝑥 ∈ On → (𝐷 = ∅ → (∀𝑦𝑥 𝐻 ≠ ∅ → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))))
9291imp4a 423 . . . . . . . . . 10 (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → (𝑥 ∈ On → ((𝐷 = ∅ ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏)))
9392com3l 89 . . . . . . . . 9 (𝑥 ∈ On → ((𝐷 = ∅ ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏)))
9493rexlimiv 3285 . . . . . . . 8 (∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦𝑥 𝐻 ≠ ∅) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))
955, 17, 943syl 18 . . . . . . 7 ((𝑅 Po 𝐴𝑤 We 𝐴) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))
9695adantlr 711 . . . . . 6 (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))
9796pm2.43i 52 . . . . 5 (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏)
9897expcom 414 . . . 4 (𝑤 We 𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))
9998exlimiv 1924 . . 3 (∃𝑤 𝑤 We 𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))
1001, 99sylbi 218 . 2 (𝐴 ∈ dom card → ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏))
1011003impib 1110 1 ((𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀𝑠((𝑠𝐴𝑅 Or 𝑠) → ∃𝑎𝐴𝑟𝑠 (𝑟𝑅𝑎𝑟 = 𝑎))) → ∃𝑎𝐴𝑏𝐴 ¬ 𝑎𝑅𝑏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 207  wa 396  wo 843  w3a 1081  wal 1528   = wceq 1530  wex 1773  wcel 2107  wne 3021  wral 3143  wrex 3144  {crab 3147  Vcvv 3500  wss 3940  c0 4295   class class class wbr 5063  cmpt 5143   Po wpo 5471   Or wor 5472   We wwe 5512  dom cdm 5554  ran crn 5555  cima 5557  Oncon0 6190  Fun wfun 6348   Fn wfn 6349  crio 7107  recscrecs 8003  cardccrd 9358
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 2798  ax-rep 5187  ax-sep 5200  ax-nul 5207  ax-pow 5263  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-ne 3022  df-ral 3148  df-rex 3149  df-reu 3150  df-rmo 3151  df-rab 3152  df-v 3502  df-sbc 3777  df-csb 3888  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-pss 3958  df-nul 4296  df-if 4471  df-pw 4544  df-sn 4565  df-pr 4567  df-tp 4569  df-op 4571  df-uni 4838  df-int 4875  df-iun 4919  df-br 5064  df-opab 5126  df-mpt 5144  df-tr 5170  df-id 5459  df-eprel 5464  df-po 5473  df-so 5474  df-fr 5513  df-se 5514  df-we 5515  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-rn 5565  df-res 5566  df-ima 5567  df-pred 6147  df-ord 6193  df-on 6194  df-suc 6196  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fo 6360  df-f1o 6361  df-fv 6362  df-isom 6363  df-riota 7108  df-wrecs 7943  df-recs 8004  df-en 8504  df-card 9362
This theorem is referenced by:  zorn2g  9919
  Copyright terms: Public domain W3C validator