Step | Hyp | Ref
| Expression |
1 | | poeq2 5456 |
. . . 4
⊢ (𝑥 = ∅ → (𝑅 Po 𝑥 ↔ 𝑅 Po ∅)) |
2 | | freq2 5506 |
. . . 4
⊢ (𝑥 = ∅ → (𝑅 Fr 𝑥 ↔ 𝑅 Fr ∅)) |
3 | 1, 2 | imbi12d 348 |
. . 3
⊢ (𝑥 = ∅ → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po ∅ → 𝑅 Fr ∅))) |
4 | | poeq2 5456 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝑦)) |
5 | | freq2 5506 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝑦)) |
6 | 4, 5 | imbi12d 348 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝑦 → 𝑅 Fr 𝑦))) |
7 | | poeq2 5456 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Po 𝑥 ↔ 𝑅 Po (𝑦 ∪ {𝑤}))) |
8 | | freq2 5506 |
. . . 4
⊢ (𝑥 = (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑥 ↔ 𝑅 Fr (𝑦 ∪ {𝑤}))) |
9 | 7, 8 | imbi12d 348 |
. . 3
⊢ (𝑥 = (𝑦 ∪ {𝑤}) → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤})))) |
10 | | poeq2 5456 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑅 Po 𝑥 ↔ 𝑅 Po 𝐴)) |
11 | | freq2 5506 |
. . . 4
⊢ (𝑥 = 𝐴 → (𝑅 Fr 𝑥 ↔ 𝑅 Fr 𝐴)) |
12 | 10, 11 | imbi12d 348 |
. . 3
⊢ (𝑥 = 𝐴 → ((𝑅 Po 𝑥 → 𝑅 Fr 𝑥) ↔ (𝑅 Po 𝐴 → 𝑅 Fr 𝐴))) |
13 | | fr0 5514 |
. . . 4
⊢ 𝑅 Fr ∅ |
14 | 13 | a1i 11 |
. . 3
⊢ (𝑅 Po ∅ → 𝑅 Fr ∅) |
15 | | ssun1 4072 |
. . . . . . 7
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑤}) |
16 | | poss 5454 |
. . . . . . 7
⊢ (𝑦 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦)) |
17 | 15, 16 | ax-mp 5 |
. . . . . 6
⊢ (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑦) |
18 | 17 | imim1i 63 |
. . . . 5
⊢ ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr 𝑦)) |
19 | | uncom 4053 |
. . . . . . . . . . . 12
⊢ (𝑦 ∪ {𝑤}) = ({𝑤} ∪ 𝑦) |
20 | 19 | sseq2i 3916 |
. . . . . . . . . . 11
⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ 𝑥 ⊆ ({𝑤} ∪ 𝑦)) |
21 | | ssundif 4384 |
. . . . . . . . . . 11
⊢ (𝑥 ⊆ ({𝑤} ∪ 𝑦) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦) |
22 | 20, 21 | bitri 278 |
. . . . . . . . . 10
⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) ↔ (𝑥 ∖ {𝑤}) ⊆ 𝑦) |
23 | 22 | anbi1i 627 |
. . . . . . . . 9
⊢ ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) ↔ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) |
24 | | breq1 5043 |
. . . . . . . . . . . . . 14
⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑤 ↔ 𝑧𝑅𝑤)) |
25 | 24 | cbvrexvw 3351 |
. . . . . . . . . . . . 13
⊢
(∃𝑣 ∈
𝑥 𝑣𝑅𝑤 ↔ ∃𝑧 ∈ 𝑥 𝑧𝑅𝑤) |
26 | | simpllr 776 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑅 Fr 𝑦) |
27 | | simplrl 777 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ⊆ 𝑦) |
28 | | poss 5454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ⊆ (𝑦 ∪ {𝑤}) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Po 𝑥)) |
29 | 28 | impcom 411 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑥 ⊆ (𝑦 ∪ {𝑤})) → 𝑅 Po 𝑥) |
30 | 22, 29 | sylan2br 598 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → 𝑅 Po 𝑥) |
31 | 30 | ad2ant2r 747 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → 𝑅 Po 𝑥) |
32 | | simpr1 1195 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ 𝑥) |
33 | | simpr2 1196 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧𝑅𝑤) |
34 | | poirr 5464 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 Po 𝑥 ∧ 𝑤 ∈ 𝑥) → ¬ 𝑤𝑅𝑤) |
35 | 34 | 3ad2antr3 1191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ¬ 𝑤𝑅𝑤) |
36 | | nbrne2 5060 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑧𝑅𝑤 ∧ ¬ 𝑤𝑅𝑤) → 𝑧 ≠ 𝑤) |
37 | 33, 35, 36 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ≠ 𝑤) |
38 | | eldifsn 4685 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) ↔ (𝑧 ∈ 𝑥 ∧ 𝑧 ≠ 𝑤)) |
39 | 32, 37, 38 | sylanbrc 586 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤})) |
40 | 31, 39 | sylan 583 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → 𝑧 ∈ (𝑥 ∖ {𝑤})) |
41 | 40 | ne0d 4234 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (𝑥 ∖ {𝑤}) ≠ ∅) |
42 | | difss 4032 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∖ {𝑤}) ⊆ 𝑥 |
43 | | vex 3404 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝑥 ∈ V |
44 | 43 | difexi 5206 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∖ {𝑤}) ∈ V |
45 | | fri 5496 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∖ {𝑤}) ∈ V ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) |
46 | 44, 45 | mpanl1 700 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) |
47 | | ssrexv 3954 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∖ {𝑤}) ⊆ 𝑥 → (∃𝑢 ∈ (𝑥 ∖ {𝑤})∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)) |
48 | 42, 46, 47 | mpsyl 68 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Fr 𝑦 ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ (𝑥 ∖ {𝑤}) ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) |
49 | 26, 27, 41, 48 | syl12anc 836 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) |
50 | | breq1 5043 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑣 = 𝑧 → (𝑣𝑅𝑢 ↔ 𝑧𝑅𝑢)) |
51 | 50 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 = 𝑧 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑧𝑅𝑢)) |
52 | 51 | rspcv 3524 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ (𝑥 ∖ {𝑤}) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢)) |
53 | 39, 52 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢)) |
54 | 53 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ¬ 𝑧𝑅𝑢)) |
55 | | simplr2 1217 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧𝑅𝑤) |
56 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑅 Po 𝑥) |
57 | | simplr1 1216 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑧 ∈ 𝑥) |
58 | | simplr3 1218 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑤 ∈ 𝑥) |
59 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → 𝑢 ∈ 𝑥) |
60 | | potr 5465 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥 ∧ 𝑢 ∈ 𝑥)) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢)) |
61 | 56, 57, 58, 59, 60 | syl13anc 1373 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → ((𝑧𝑅𝑤 ∧ 𝑤𝑅𝑢) → 𝑧𝑅𝑢)) |
62 | 55, 61 | mpand 695 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (𝑤𝑅𝑢 → 𝑧𝑅𝑢)) |
63 | 62 | con3d 155 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ¬ 𝑤𝑅𝑢)) |
64 | | vex 3404 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝑤 ∈ V |
65 | | breq1 5043 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑣 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑤𝑅𝑢)) |
66 | 65 | notbid 321 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑣 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢)) |
67 | 64, 66 | ralsn 4582 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑣 ∈
{𝑤} ¬ 𝑣𝑅𝑢 ↔ ¬ 𝑤𝑅𝑢) |
68 | 63, 67 | syl6ibr 255 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (¬ 𝑧𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢)) |
69 | 54, 68 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢)) |
70 | | ralun 4092 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((∀𝑣 ∈
(𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ∧ ∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢) → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢) |
71 | 70 | ex 416 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(∀𝑣 ∈
(𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → (∀𝑣 ∈ {𝑤} ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)) |
72 | 69, 71 | sylcom 30 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢)) |
73 | | difsnid 4708 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ 𝑥 → ((𝑥 ∖ {𝑤}) ∪ {𝑤}) = 𝑥) |
74 | 73 | raleqdv 3317 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 ∈ 𝑥 → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
75 | 58, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ ((𝑥 ∖ {𝑤}) ∪ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
76 | 72, 75 | sylibd 242 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) ∧ 𝑢 ∈ 𝑥) → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
77 | 76 | reximdva 3185 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑅 Po 𝑥 ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
78 | 31, 77 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
79 | 49, 78 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) ∧ (𝑧 ∈ 𝑥 ∧ 𝑧𝑅𝑤 ∧ 𝑤 ∈ 𝑥)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢) |
80 | 79 | 3exp2 1355 |
. . . . . . . . . . . . . 14
⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑧 ∈ 𝑥 → (𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)))) |
81 | 80 | rexlimdv 3194 |
. . . . . . . . . . . . 13
⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑧 ∈ 𝑥 𝑧𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))) |
82 | 25, 81 | syl5bi 245 |
. . . . . . . . . . . 12
⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))) |
83 | | ralnex 3150 |
. . . . . . . . . . . . 13
⊢
(∀𝑣 ∈
𝑥 ¬ 𝑣𝑅𝑤 ↔ ¬ ∃𝑣 ∈ 𝑥 𝑣𝑅𝑤) |
84 | | breq2 5044 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑢 = 𝑤 → (𝑣𝑅𝑢 ↔ 𝑣𝑅𝑤)) |
85 | 84 | notbid 321 |
. . . . . . . . . . . . . . . 16
⊢ (𝑢 = 𝑤 → (¬ 𝑣𝑅𝑢 ↔ ¬ 𝑣𝑅𝑤)) |
86 | 85 | ralbidv 3110 |
. . . . . . . . . . . . . . 15
⊢ (𝑢 = 𝑤 → (∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤)) |
87 | 86 | rspcev 3529 |
. . . . . . . . . . . . . 14
⊢ ((𝑤 ∈ 𝑥 ∧ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑤) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢) |
88 | 87 | expcom 417 |
. . . . . . . . . . . . 13
⊢
(∀𝑣 ∈
𝑥 ¬ 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
89 | 83, 88 | sylbir 238 |
. . . . . . . . . . . 12
⊢ (¬
∃𝑣 ∈ 𝑥 𝑣𝑅𝑤 → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
90 | 82, 89 | pm2.61d1 183 |
. . . . . . . . . . 11
⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
91 | | difsn 4696 |
. . . . . . . . . . . 12
⊢ (¬
𝑤 ∈ 𝑥 → (𝑥 ∖ {𝑤}) = 𝑥) |
92 | 48 | expr 460 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢)) |
93 | | neeq1 2997 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → ((𝑥 ∖ {𝑤}) ≠ ∅ ↔ 𝑥 ≠ ∅)) |
94 | | raleq 3311 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
95 | 94 | rexbidv 3208 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢 ↔ ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
96 | 93, 95 | imbi12d 348 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∖ {𝑤}) = 𝑥 → (((𝑥 ∖ {𝑤}) ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ (𝑥 ∖ {𝑤}) ¬ 𝑣𝑅𝑢) ↔ (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))) |
97 | 92, 96 | syl5ibcom 248 |
. . . . . . . . . . . . . . 15
⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → ((𝑥 ∖ {𝑤}) = 𝑥 → (𝑥 ≠ ∅ → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))) |
98 | 97 | com23 86 |
. . . . . . . . . . . . . 14
⊢ ((𝑅 Fr 𝑦 ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))) |
99 | 98 | adantll 714 |
. . . . . . . . . . . . 13
⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ (𝑥 ∖ {𝑤}) ⊆ 𝑦) → (𝑥 ≠ ∅ → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢))) |
100 | 99 | impr 458 |
. . . . . . . . . . . 12
⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ((𝑥 ∖ {𝑤}) = 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
101 | 91, 100 | syl5 34 |
. . . . . . . . . . 11
⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → (¬ 𝑤 ∈ 𝑥 → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
102 | 90, 101 | pm2.61d 182 |
. . . . . . . . . 10
⊢ (((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) ∧ ((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅)) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢) |
103 | 102 | ex 416 |
. . . . . . . . 9
⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → (((𝑥 ∖ {𝑤}) ⊆ 𝑦 ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
104 | 23, 103 | syl5bi 245 |
. . . . . . . 8
⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
105 | 104 | alrimiv 1934 |
. . . . . . 7
⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
106 | | df-fr 5493 |
. . . . . . 7
⊢ (𝑅 Fr (𝑦 ∪ {𝑤}) ↔ ∀𝑥((𝑥 ⊆ (𝑦 ∪ {𝑤}) ∧ 𝑥 ≠ ∅) → ∃𝑢 ∈ 𝑥 ∀𝑣 ∈ 𝑥 ¬ 𝑣𝑅𝑢)) |
107 | 105, 106 | sylibr 237 |
. . . . . 6
⊢ ((𝑅 Po (𝑦 ∪ {𝑤}) ∧ 𝑅 Fr 𝑦) → 𝑅 Fr (𝑦 ∪ {𝑤})) |
108 | 107 | ex 416 |
. . . . 5
⊢ (𝑅 Po (𝑦 ∪ {𝑤}) → (𝑅 Fr 𝑦 → 𝑅 Fr (𝑦 ∪ {𝑤}))) |
109 | 18, 108 | sylcom 30 |
. . . 4
⊢ ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤}))) |
110 | 109 | a1i 11 |
. . 3
⊢ (𝑦 ∈ Fin → ((𝑅 Po 𝑦 → 𝑅 Fr 𝑦) → (𝑅 Po (𝑦 ∪ {𝑤}) → 𝑅 Fr (𝑦 ∪ {𝑤})))) |
111 | 3, 6, 9, 12, 14, 110 | findcard2 8776 |
. 2
⊢ (𝐴 ∈ Fin → (𝑅 Po 𝐴 → 𝑅 Fr 𝐴)) |
112 | 111 | impcom 411 |
1
⊢ ((𝑅 Po 𝐴 ∧ 𝐴 ∈ Fin) → 𝑅 Fr 𝐴) |