Step | Hyp | Ref
| Expression |
1 | | weso 5029 |
. . . 4
⊢ (𝑅 We 𝐴 → 𝑅 Or 𝐴) |
2 | | socnv 30908 |
. . . 4
⊢ (𝑅 Or 𝐴 → ◡𝑅 Or 𝐴) |
3 | 1, 2 | syl 17 |
. . 3
⊢ (𝑅 We 𝐴 → ◡𝑅 Or 𝐴) |
4 | 3 | 3ad2ant1 1075 |
. 2
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → ◡𝑅 Or 𝐴) |
5 | | simp1 1054 |
. . . 4
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → 𝑅 We 𝐴) |
6 | | simp2 1055 |
. . . 4
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → 𝑅 Se 𝐴) |
7 | | ssid 3587 |
. . . . 5
⊢ 𝐴 ⊆ 𝐴 |
8 | 7 | a1i 11 |
. . . 4
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → 𝐴 ⊆ 𝐴) |
9 | | simp3 1056 |
. . . 4
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → 𝐴 ≠ ∅) |
10 | | tz6.26 5628 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴) ∧ (𝐴 ⊆ 𝐴 ∧ 𝐴 ≠ ∅)) → ∃𝑥 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑥) = ∅) |
11 | 5, 6, 8, 9, 10 | syl22anc 1319 |
. . 3
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑥) = ∅) |
12 | | pm2.27 41 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑥) → ¬ 𝑦𝑅𝑥)) |
13 | 12 | ad2antll 761 |
. . . . . . . . . 10
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑥) → ¬ 𝑦𝑅𝑥)) |
14 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (𝑦◡𝑅𝑧 ↔ 𝑦◡𝑅𝑥)) |
15 | 14 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦◡𝑅𝑥) → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧) |
16 | 15 | ex 449 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝐴 → (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)) |
17 | 16 | ad2antrl 760 |
. . . . . . . . . 10
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)) |
18 | 13, 17 | jctird 565 |
. . . . . . . . 9
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑥) → (¬ 𝑦𝑅𝑥 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)))) |
19 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
20 | | vex 3176 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
21 | 20 | elpred 5610 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ V → (𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑥))) |
22 | 19, 21 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) ↔ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑥)) |
23 | 22 | notbii 309 |
. . . . . . . . . 10
⊢ (¬
𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) ↔ ¬ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑥)) |
24 | | imnan 437 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑥) ↔ ¬ (𝑦 ∈ 𝐴 ∧ 𝑦𝑅𝑥)) |
25 | 23, 24 | bitr4i 266 |
. . . . . . . . 9
⊢ (¬
𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑥)) |
26 | 19, 20 | brcnv 5227 |
. . . . . . . . . . 11
⊢ (𝑥◡𝑅𝑦 ↔ 𝑦𝑅𝑥) |
27 | 26 | notbii 309 |
. . . . . . . . . 10
⊢ (¬
𝑥◡𝑅𝑦 ↔ ¬ 𝑦𝑅𝑥) |
28 | 27 | anbi1i 727 |
. . . . . . . . 9
⊢ ((¬
𝑥◡𝑅𝑦 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)) ↔ (¬ 𝑦𝑅𝑥 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧))) |
29 | 18, 25, 28 | 3imtr4g 284 |
. . . . . . . 8
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) → (¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) → (¬ 𝑥◡𝑅𝑦 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)))) |
30 | 29 | expr 641 |
. . . . . . 7
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∈ 𝐴 → (¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) → (¬ 𝑥◡𝑅𝑦 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧))))) |
31 | 30 | com23 84 |
. . . . . 6
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) → (𝑦 ∈ 𝐴 → (¬ 𝑥◡𝑅𝑦 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧))))) |
32 | 31 | alimdv 1832 |
. . . . 5
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (∀𝑦 ¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥) → ∀𝑦(𝑦 ∈ 𝐴 → (¬ 𝑥◡𝑅𝑦 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧))))) |
33 | | eq0 3888 |
. . . . 5
⊢
(Pred(𝑅, 𝐴, 𝑥) = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ Pred(𝑅, 𝐴, 𝑥)) |
34 | | r19.26 3046 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 (¬ 𝑥◡𝑅𝑦 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧))) |
35 | | df-ral 2901 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 (¬ 𝑥◡𝑅𝑦 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (¬ 𝑥◡𝑅𝑦 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)))) |
36 | 34, 35 | bitr3i 265 |
. . . . 5
⊢
((∀𝑦 ∈
𝐴 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)) ↔ ∀𝑦(𝑦 ∈ 𝐴 → (¬ 𝑥◡𝑅𝑦 ∧ (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)))) |
37 | 32, 33, 36 | 3imtr4g 284 |
. . . 4
⊢ (((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) ∧ 𝑥 ∈ 𝐴) → (Pred(𝑅, 𝐴, 𝑥) = ∅ → (∀𝑦 ∈ 𝐴 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)))) |
38 | 37 | reximdva 3000 |
. . 3
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → (∃𝑥 ∈ 𝐴 Pred(𝑅, 𝐴, 𝑥) = ∅ → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧)))) |
39 | 11, 38 | mpd 15 |
. 2
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → ∃𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 ¬ 𝑥◡𝑅𝑦 ∧ ∀𝑦 ∈ 𝐴 (𝑦◡𝑅𝑥 → ∃𝑧 ∈ 𝐴 𝑦◡𝑅𝑧))) |
40 | 4, 39 | supcl 8247 |
1
⊢ ((𝑅 We 𝐴 ∧ 𝑅 Se 𝐴 ∧ 𝐴 ≠ ∅) → sup(𝐴, 𝐴, ◡𝑅) ∈ 𝐴) |