Proof of Theorem zorn2lem7
Step | Hyp | Ref
| Expression |
1 | | ween 9535 |
. . 3
⊢ (𝐴 ∈ dom card ↔
∃𝑤 𝑤 We 𝐴) |
2 | | zorn2lem.3 |
. . . . . . . . 9
⊢ 𝐹 = recs((𝑓 ∈ V ↦ (℩𝑣 ∈ 𝐶 ∀𝑢 ∈ 𝐶 ¬ 𝑢𝑤𝑣))) |
3 | | zorn2lem.4 |
. . . . . . . . 9
⊢ 𝐶 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ ran 𝑓 𝑔𝑅𝑧} |
4 | | zorn2lem.5 |
. . . . . . . . 9
⊢ 𝐷 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} |
5 | 2, 3, 4 | zorn2lem4 9999 |
. . . . . . . 8
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → ∃𝑥 ∈ On 𝐷 = ∅) |
6 | | imaeq2 5899 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (𝐹 “ 𝑥) = (𝐹 “ 𝑦)) |
7 | 6 | raleqdv 3316 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑦 → (∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧 ↔ ∀𝑔 ∈ (𝐹 “ 𝑦)𝑔𝑅𝑧)) |
8 | 7 | rabbidv 3381 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑦)𝑔𝑅𝑧}) |
9 | | zorn2lem.7 |
. . . . . . . . . . . 12
⊢ 𝐻 = {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑦)𝑔𝑅𝑧} |
10 | 8, 4, 9 | 3eqtr4g 2798 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 𝐷 = 𝐻) |
11 | 10 | eqeq1d 2740 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝐷 = ∅ ↔ 𝐻 = ∅)) |
12 | 11 | onminex 7541 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
𝐷 = ∅ →
∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ 𝐻 = ∅)) |
13 | | df-ne 2935 |
. . . . . . . . . . . 12
⊢ (𝐻 ≠ ∅ ↔ ¬ 𝐻 = ∅) |
14 | 13 | ralbii 3080 |
. . . . . . . . . . 11
⊢
(∀𝑦 ∈
𝑥 𝐻 ≠ ∅ ↔ ∀𝑦 ∈ 𝑥 ¬ 𝐻 = ∅) |
15 | 14 | anbi2i 626 |
. . . . . . . . . 10
⊢ ((𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) ↔ (𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ 𝐻 = ∅)) |
16 | 15 | rexbii 3161 |
. . . . . . . . 9
⊢
(∃𝑥 ∈ On
(𝐷 = ∅ ∧
∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) ↔ ∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 ¬ 𝐻 = ∅)) |
17 | 12, 16 | sylibr 237 |
. . . . . . . 8
⊢
(∃𝑥 ∈ On
𝐷 = ∅ →
∃𝑥 ∈ On (𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) |
18 | 2, 3, 4, 9 | zorn2lem5 10000 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (𝐹 “ 𝑥) ⊆ 𝐴) |
19 | 18 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 Po 𝐴 → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (𝐹 “ 𝑥) ⊆ 𝐴)) |
20 | 2, 3, 4, 9 | zorn2lem6 10001 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑅 Po 𝐴 → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → 𝑅 Or (𝐹 “ 𝑥))) |
21 | 19, 20 | jcad 516 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑅 Po 𝐴 → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → ((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝑅 Or (𝐹 “ 𝑥)))) |
22 | 2 | tfr1 8062 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐹 Fn On |
23 | | fnfun 6438 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐹 Fn On → Fun 𝐹) |
24 | | vex 3402 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 𝑥 ∈ V |
25 | 24 | funimaex 6426 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (Fun
𝐹 → (𝐹 “ 𝑥) ∈ V) |
26 | 22, 23, 25 | mp2b 10 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝐹 “ 𝑥) ∈ V |
27 | | sseq1 3902 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑥) → (𝑠 ⊆ 𝐴 ↔ (𝐹 “ 𝑥) ⊆ 𝐴)) |
28 | | soeq2 5464 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑥) → (𝑅 Or 𝑠 ↔ 𝑅 Or (𝐹 “ 𝑥))) |
29 | 27, 28 | anbi12d 634 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝐹 “ 𝑥) → ((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) ↔ ((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝑅 Or (𝐹 “ 𝑥)))) |
30 | | raleq 3310 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 = (𝐹 “ 𝑥) → (∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) ↔ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
31 | 30 | rexbidv 3207 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 = (𝐹 “ 𝑥) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) ↔ ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
32 | 29, 31 | imbi12d 348 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑠 = (𝐹 “ 𝑥) → (((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) ↔ (((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝑅 Or (𝐹 “ 𝑥)) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)))) |
33 | 26, 32 | spcv 3509 |
. . . . . . . . . . . . . . . . . 18
⊢
(∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → (((𝐹 “ 𝑥) ⊆ 𝐴 ∧ 𝑅 Or (𝐹 “ 𝑥)) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
34 | 21, 33 | sylan9 511 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
35 | 34 | adantld 494 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ((𝐷 = ∅ ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) |
36 | 35 | imp 410 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ (𝐷 = ∅ ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) |
37 | | noel 4219 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ¬
𝑏 ∈
∅ |
38 | 18 | sseld 3876 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (𝑟 ∈ (𝐹 “ 𝑥) → 𝑟 ∈ 𝐴)) |
39 | | 3anass 1096 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑟 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) ↔ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) |
40 | | potr 5455 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . . 47
⊢ ((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → ((𝑟𝑅𝑎 ∧ 𝑎𝑅𝑏) → 𝑟𝑅𝑏)) |
41 | 39, 40 | sylan2br 598 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ ((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) → ((𝑟𝑅𝑎 ∧ 𝑎𝑅𝑏) → 𝑟𝑅𝑏)) |
42 | 41 | expcomd 420 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ ((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) → (𝑎𝑅𝑏 → (𝑟𝑅𝑎 → 𝑟𝑅𝑏))) |
43 | 42 | imp 410 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ 𝑎𝑅𝑏) → (𝑟𝑅𝑎 → 𝑟𝑅𝑏)) |
44 | | breq1 5033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . . 46
⊢ (𝑟 = 𝑎 → (𝑟𝑅𝑏 ↔ 𝑎𝑅𝑏)) |
45 | 44 | biimprcd 253 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . . 45
⊢ (𝑎𝑅𝑏 → (𝑟 = 𝑎 → 𝑟𝑅𝑏)) |
46 | 45 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . . 44
⊢ (((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ 𝑎𝑅𝑏) → (𝑟 = 𝑎 → 𝑟𝑅𝑏)) |
47 | 43, 46 | jaod 858 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . . 43
⊢ (((𝑅 Po 𝐴 ∧ (𝑟 ∈ 𝐴 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ 𝑎𝑅𝑏) → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏)) |
48 | 47 | exp42 439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑅 Po 𝐴 → (𝑟 ∈ 𝐴 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑎𝑅𝑏 → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))))) |
49 | 38, 48 | sylan9r 512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑟 ∈ (𝐹 “ 𝑥) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑎𝑅𝑏 → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))))) |
50 | 49 | com24 95 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑎𝑅𝑏 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑟 ∈ (𝐹 “ 𝑥) → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))))) |
51 | 50 | com23 86 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (𝑎𝑅𝑏 → (𝑟 ∈ (𝐹 “ 𝑥) → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))))) |
52 | 51 | imp31 421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑎𝑅𝑏) → (𝑟 ∈ (𝐹 “ 𝑥) → ((𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑟𝑅𝑏))) |
53 | 52 | a2d 29 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑎𝑅𝑏) → ((𝑟 ∈ (𝐹 “ 𝑥) → (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → (𝑟 ∈ (𝐹 “ 𝑥) → 𝑟𝑅𝑏))) |
54 | 53 | ralimdv2 3090 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑎𝑅𝑏) → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∀𝑟 ∈ (𝐹 “ 𝑥)𝑟𝑅𝑏)) |
55 | | breq1 5033 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝑟 = 𝑔 → (𝑟𝑅𝑏 ↔ 𝑔𝑅𝑏)) |
56 | 55 | cbvralvw 3349 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢
(∀𝑟 ∈
(𝐹 “ 𝑥)𝑟𝑅𝑏 ↔ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏) |
57 | | breq2 5034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . . 42
⊢ (𝑧 = 𝑏 → (𝑔𝑅𝑧 ↔ 𝑔𝑅𝑏)) |
58 | 57 | ralbidv 3109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝑧 = 𝑏 → (∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧 ↔ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏)) |
59 | 58 | elrab 3588 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝑏 ∈ {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} ↔ (𝑏 ∈ 𝐴 ∧ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏)) |
60 | 4 | eqeq1i 2743 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ (𝐷 = ∅ ↔ {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} = ∅) |
61 | | eleq2 2821 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . . 41
⊢ ({𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} = ∅ → (𝑏 ∈ {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} ↔ 𝑏 ∈ ∅)) |
62 | 60, 61 | sylbi 220 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . . 40
⊢ (𝐷 = ∅ → (𝑏 ∈ {𝑧 ∈ 𝐴 ∣ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑧} ↔ 𝑏 ∈ ∅)) |
63 | 59, 62 | bitr3id 288 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . . 39
⊢ (𝐷 = ∅ → ((𝑏 ∈ 𝐴 ∧ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏) ↔ 𝑏 ∈ ∅)) |
64 | 63 | biimpd 232 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ (𝐷 = ∅ → ((𝑏 ∈ 𝐴 ∧ ∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏) → 𝑏 ∈ ∅)) |
65 | 64 | expdimp 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → (∀𝑔 ∈ (𝐹 “ 𝑥)𝑔𝑅𝑏 → 𝑏 ∈ ∅)) |
66 | 56, 65 | syl5bi 245 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → (∀𝑟 ∈ (𝐹 “ 𝑥)𝑟𝑅𝑏 → 𝑏 ∈ ∅)) |
67 | 54, 66 | sylan9r 512 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) ∧ (((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) ∧ 𝑎𝑅𝑏)) → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑏 ∈ ∅)) |
68 | 67 | exp32 424 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → (((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (𝑎𝑅𝑏 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → 𝑏 ∈ ∅)))) |
69 | 68 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → (((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴)) → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → (𝑎𝑅𝑏 → 𝑏 ∈ ∅)))) |
70 | 69 | imp31 421 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) ∧ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → (𝑎𝑅𝑏 → 𝑏 ∈ ∅)) |
71 | 37, 70 | mtoi 202 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) ∧ ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴))) ∧ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → ¬ 𝑎𝑅𝑏) |
72 | 71 | exp42 439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐴) → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))) |
73 | 72 | exp4a 435 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑎 ∈ 𝐴 → (𝑏 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))) |
74 | 73 | com34 91 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐷 = ∅ ∧ 𝑏 ∈ 𝐴) → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑏 ∈ 𝐴 → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))) |
75 | 74 | ex 416 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐷 = ∅ → (𝑏 ∈ 𝐴 → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑏 ∈ 𝐴 → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))))) |
76 | 75 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑏 ∈ 𝐴 → (𝐷 = ∅ → (𝑏 ∈ 𝐴 → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))))) |
77 | 76 | pm2.43a 54 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑏 ∈ 𝐴 → (𝐷 = ∅ → ((𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅)) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏))))) |
78 | 77 | impd 414 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ∈ 𝐴 → ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ¬ 𝑎𝑅𝑏)))) |
79 | 78 | com4l 92 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → (𝑏 ∈ 𝐴 → ¬ 𝑎𝑅𝑏)))) |
80 | 79 | impd 414 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → ((𝑎 ∈ 𝐴 ∧ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → (𝑏 ∈ 𝐴 → ¬ 𝑎𝑅𝑏))) |
81 | 80 | ralrimdv 3100 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → ((𝑎 ∈ 𝐴 ∧ ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎)) → ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
82 | 81 | expd 419 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (𝑎 ∈ 𝐴 → (∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏))) |
83 | 82 | reximdvai 3182 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 = ∅ ∧ (𝑅 Po 𝐴 ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
84 | 83 | exp32 424 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐷 = ∅ → (𝑅 Po 𝐴 → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
85 | 84 | com12 32 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑅 Po 𝐴 → (𝐷 = ∅ → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
86 | 85 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → (𝐷 = ∅ → (((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
87 | 86 | imp32 422 |
. . . . . . . . . . . . . . 15
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ (𝐷 = ∅ ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → (∃𝑎 ∈ 𝐴 ∀𝑟 ∈ (𝐹 “ 𝑥)(𝑟𝑅𝑎 ∨ 𝑟 = 𝑎) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
88 | 36, 87 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ (𝐷 = ∅ ∧ ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏) |
89 | 88 | exp45 442 |
. . . . . . . . . . . . 13
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → (𝐷 = ∅ → ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) → (∀𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
90 | 89 | com23 86 |
. . . . . . . . . . . 12
⊢ ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ((𝑤 We 𝐴 ∧ 𝑥 ∈ On) → (𝐷 = ∅ → (∀𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
91 | 90 | expdimp 456 |
. . . . . . . . . . 11
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → (𝑥 ∈ On → (𝐷 = ∅ → (∀𝑦 ∈ 𝑥 𝐻 ≠ ∅ → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)))) |
92 | 91 | imp4a 426 |
. . . . . . . . . 10
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → (𝑥 ∈ On → ((𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏))) |
93 | 92 | com3l 89 |
. . . . . . . . 9
⊢ (𝑥 ∈ On → ((𝐷 = ∅ ∧ ∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏))) |
94 | 93 | rexlimiv 3190 |
. . . . . . . 8
⊢
(∃𝑥 ∈ On
(𝐷 = ∅ ∧
∀𝑦 ∈ 𝑥 𝐻 ≠ ∅) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
95 | 5, 17, 94 | 3syl 18 |
. . . . . . 7
⊢ ((𝑅 Po 𝐴 ∧ 𝑤 We 𝐴) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
96 | 95 | adantlr 715 |
. . . . . 6
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
97 | 96 | pm2.43i 52 |
. . . . 5
⊢ (((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) ∧ 𝑤 We 𝐴) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏) |
98 | 97 | expcom 417 |
. . . 4
⊢ (𝑤 We 𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
99 | 98 | exlimiv 1937 |
. . 3
⊢
(∃𝑤 𝑤 We 𝐴 → ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
100 | 1, 99 | sylbi 220 |
. 2
⊢ (𝐴 ∈ dom card → ((𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏)) |
101 | 100 | 3impib 1117 |
1
⊢ ((𝐴 ∈ dom card ∧ 𝑅 Po 𝐴 ∧ ∀𝑠((𝑠 ⊆ 𝐴 ∧ 𝑅 Or 𝑠) → ∃𝑎 ∈ 𝐴 ∀𝑟 ∈ 𝑠 (𝑟𝑅𝑎 ∨ 𝑟 = 𝑎))) → ∃𝑎 ∈ 𝐴 ∀𝑏 ∈ 𝐴 ¬ 𝑎𝑅𝑏) |