Step | Hyp | Ref
| Expression |
1 | | po0 5050 |
. . . 4
⊢ 𝑅 Po ∅ |
2 | | res0 5400 |
. . . . . . 7
⊢ ( I
↾ ∅) = ∅ |
3 | 2 | ineq2i 3811 |
. . . . . 6
⊢ (𝑅 ∩ ( I ↾ ∅)) =
(𝑅 ∩
∅) |
4 | | in0 3968 |
. . . . . 6
⊢ (𝑅 ∩ ∅) =
∅ |
5 | 3, 4 | eqtri 2644 |
. . . . 5
⊢ (𝑅 ∩ ( I ↾ ∅)) =
∅ |
6 | | xp0 5552 |
. . . . . . . . . 10
⊢ (𝐴 × ∅) =
∅ |
7 | 6 | ineq2i 3811 |
. . . . . . . . 9
⊢ (𝑅 ∩ (𝐴 × ∅)) = (𝑅 ∩ ∅) |
8 | 7, 4 | eqtri 2644 |
. . . . . . . 8
⊢ (𝑅 ∩ (𝐴 × ∅)) =
∅ |
9 | 8 | coeq2i 5282 |
. . . . . . 7
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) |
10 | | co02 5649 |
. . . . . . 7
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ ∅) =
∅ |
11 | 9, 10 | eqtri 2644 |
. . . . . 6
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) =
∅ |
12 | | 0ss 3972 |
. . . . . 6
⊢ ∅
⊆ 𝑅 |
13 | 11, 12 | eqsstri 3635 |
. . . . 5
⊢ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅 |
14 | 5, 13 | pm3.2i 471 |
. . . 4
⊢ ((𝑅 ∩ ( I ↾ ∅)) =
∅ ∧ ((𝑅 ∩
(𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅) |
15 | 1, 14 | 2th 254 |
. . 3
⊢ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) =
∅ ∧ ((𝑅 ∩
(𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)) |
16 | | poeq2 5039 |
. . . 4
⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ 𝑅 Po ∅)) |
17 | | reseq2 5391 |
. . . . . . 7
⊢ (𝐴 = ∅ → ( I ↾
𝐴) = ( I ↾
∅)) |
18 | 17 | ineq2d 3814 |
. . . . . 6
⊢ (𝐴 = ∅ → (𝑅 ∩ ( I ↾ 𝐴)) = (𝑅 ∩ ( I ↾
∅))) |
19 | 18 | eqeq1d 2624 |
. . . . 5
⊢ (𝐴 = ∅ → ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔ (𝑅 ∩ ( I ↾ ∅)) =
∅)) |
20 | | xpeq2 5129 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (𝐴 × 𝐴) = (𝐴 × ∅)) |
21 | 20 | ineq2d 3814 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝑅 ∩ (𝐴 × 𝐴)) = (𝑅 ∩ (𝐴 × ∅))) |
22 | 21 | coeq2d 5284 |
. . . . . 6
⊢ (𝐴 = ∅ → ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) = ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅)))) |
23 | 22 | sseq1d 3632 |
. . . . 5
⊢ (𝐴 = ∅ → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)) |
24 | 19, 23 | anbi12d 747 |
. . . 4
⊢ (𝐴 = ∅ → (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧
((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅))) |
25 | 16, 24 | bibi12d 335 |
. . 3
⊢ (𝐴 = ∅ → ((𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) ↔ (𝑅 Po ∅ ↔ ((𝑅 ∩ ( I ↾ ∅)) = ∅ ∧
((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × ∅))) ⊆ 𝑅)))) |
26 | 15, 25 | mpbiri 248 |
. 2
⊢ (𝐴 = ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))) |
27 | | r19.28zv 4066 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ →
(∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) |
28 | 27 | ralbidv 2986 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) |
29 | | r19.28zv 4066 |
. . . . . 6
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) |
30 | 28, 29 | bitrd 268 |
. . . . 5
⊢ (𝐴 ≠ ∅ →
(∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) |
31 | 30 | ralbidv 2986 |
. . . 4
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ ∀𝑥 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) |
32 | | r19.26 3064 |
. . . 4
⊢
(∀𝑥 ∈
𝐴 (¬ 𝑥𝑅𝑥 ∧ ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
33 | 31, 32 | syl6bb 276 |
. . 3
⊢ (𝐴 ≠ ∅ →
(∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)))) |
34 | | df-po 5035 |
. . 3
⊢ (𝑅 Po 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (¬ 𝑥𝑅𝑥 ∧ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
35 | | disj 4017 |
. . . . 5
⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔
∀𝑤 ∈ 𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴)) |
36 | | df-ral 2917 |
. . . . 5
⊢
(∀𝑤 ∈
𝑅 ¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴))) |
37 | | opex 4932 |
. . . . . . . . . 10
⊢
〈𝑥, 𝑥〉 ∈ V |
38 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ (𝑤 = 〈𝑥, 𝑥〉 → (𝑤 ∈ 𝑅 ↔ 〈𝑥, 𝑥〉 ∈ 𝑅)) |
39 | | df-br 4654 |
. . . . . . . . . . . 12
⊢ (𝑥𝑅𝑥 ↔ 〈𝑥, 𝑥〉 ∈ 𝑅) |
40 | 38, 39 | syl6bbr 278 |
. . . . . . . . . . 11
⊢ (𝑤 = 〈𝑥, 𝑥〉 → (𝑤 ∈ 𝑅 ↔ 𝑥𝑅𝑥)) |
41 | | eleq1 2689 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 〈𝑥, 𝑥〉 → (𝑤 ∈ ( I ↾ 𝐴) ↔ 〈𝑥, 𝑥〉 ∈ ( I ↾ 𝐴))) |
42 | | vex 3203 |
. . . . . . . . . . . . . . . 16
⊢ 𝑥 ∈ V |
43 | | ididg 5275 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ V → 𝑥 I 𝑥) |
44 | 42, 43 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 I 𝑥 |
45 | 42 | brres 5402 |
. . . . . . . . . . . . . . 15
⊢ (𝑥( I ↾ 𝐴)𝑥 ↔ (𝑥 I 𝑥 ∧ 𝑥 ∈ 𝐴)) |
46 | 44, 45 | mpbiran 953 |
. . . . . . . . . . . . . 14
⊢ (𝑥( I ↾ 𝐴)𝑥 ↔ 𝑥 ∈ 𝐴) |
47 | | df-br 4654 |
. . . . . . . . . . . . . 14
⊢ (𝑥( I ↾ 𝐴)𝑥 ↔ 〈𝑥, 𝑥〉 ∈ ( I ↾ 𝐴)) |
48 | 46, 47 | bitr3i 266 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ 𝐴 ↔ 〈𝑥, 𝑥〉 ∈ ( I ↾ 𝐴)) |
49 | 41, 48 | syl6bbr 278 |
. . . . . . . . . . . 12
⊢ (𝑤 = 〈𝑥, 𝑥〉 → (𝑤 ∈ ( I ↾ 𝐴) ↔ 𝑥 ∈ 𝐴)) |
50 | 49 | notbid 308 |
. . . . . . . . . . 11
⊢ (𝑤 = 〈𝑥, 𝑥〉 → (¬ 𝑤 ∈ ( I ↾ 𝐴) ↔ ¬ 𝑥 ∈ 𝐴)) |
51 | 40, 50 | imbi12d 334 |
. . . . . . . . . 10
⊢ (𝑤 = 〈𝑥, 𝑥〉 → ((𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴))) |
52 | 37, 51 | spcv 3299 |
. . . . . . . . 9
⊢
(∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥𝑅𝑥 → ¬ 𝑥 ∈ 𝐴)) |
53 | 52 | con2d 129 |
. . . . . . . 8
⊢
(∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → (𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥)) |
54 | 53 | alrimiv 1855 |
. . . . . . 7
⊢
(∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) → ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥)) |
55 | | relres 5426 |
. . . . . . . . . . . 12
⊢ Rel ( I
↾ 𝐴) |
56 | | elrel 5222 |
. . . . . . . . . . . 12
⊢ ((Rel ( I
↾ 𝐴) ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ∃𝑦∃𝑧 𝑤 = 〈𝑦, 𝑧〉) |
57 | 55, 56 | mpan 706 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ( I ↾ 𝐴) → ∃𝑦∃𝑧 𝑤 = 〈𝑦, 𝑧〉) |
58 | 57 | ancri 575 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ( I ↾ 𝐴) → (∃𝑦∃𝑧 𝑤 = 〈𝑦, 𝑧〉 ∧ 𝑤 ∈ ( I ↾ 𝐴))) |
59 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) |
60 | | breq12 4658 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 = 𝑦 ∧ 𝑥 = 𝑦) → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦)) |
61 | 60 | anidms 677 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑦 → (𝑥𝑅𝑥 ↔ 𝑦𝑅𝑦)) |
62 | 61 | notbid 308 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → (¬ 𝑥𝑅𝑥 ↔ ¬ 𝑦𝑅𝑦)) |
63 | 59, 62 | imbi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦))) |
64 | 63 | spv 2260 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦)) |
65 | | breq2 4657 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 𝑧 → (𝑦𝑅𝑦 ↔ 𝑦𝑅𝑧)) |
66 | 65 | notbid 308 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 𝑧 → (¬ 𝑦𝑅𝑦 ↔ ¬ 𝑦𝑅𝑧)) |
67 | 66 | imbi2d 330 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 𝑧 → ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) ↔ (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧))) |
68 | 67 | biimpcd 239 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → (𝑦 = 𝑧 → (𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑧))) |
69 | 68 | impd 447 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐴 → ¬ 𝑦𝑅𝑦) → ((𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦𝑅𝑧)) |
70 | 64, 69 | syl 17 |
. . . . . . . . . . . . 13
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦𝑅𝑧)) |
71 | | eleq1 2689 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (𝑤 ∈ ( I ↾ 𝐴) ↔ 〈𝑦, 𝑧〉 ∈ ( I ↾ 𝐴))) |
72 | | vex 3203 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
73 | 72 | brres 5402 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ (𝑦 I 𝑧 ∧ 𝑦 ∈ 𝐴)) |
74 | | df-br 4654 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦( I ↾ 𝐴)𝑧 ↔ 〈𝑦, 𝑧〉 ∈ ( I ↾ 𝐴)) |
75 | 72 | ideq 5274 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 I 𝑧 ↔ 𝑦 = 𝑧) |
76 | 75 | anbi1i 731 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 I 𝑧 ∧ 𝑦 ∈ 𝐴) ↔ (𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴)) |
77 | 73, 74, 76 | 3bitr3ri 291 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴) ↔ 〈𝑦, 𝑧〉 ∈ ( I ↾ 𝐴)) |
78 | 71, 77 | syl6bbr 278 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (𝑤 ∈ ( I ↾ 𝐴) ↔ (𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴))) |
79 | | eleq1 2689 |
. . . . . . . . . . . . . . . 16
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (𝑤 ∈ 𝑅 ↔ 〈𝑦, 𝑧〉 ∈ 𝑅)) |
80 | | df-br 4654 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦𝑅𝑧 ↔ 〈𝑦, 𝑧〉 ∈ 𝑅) |
81 | 79, 80 | syl6bbr 278 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (𝑤 ∈ 𝑅 ↔ 𝑦𝑅𝑧)) |
82 | 81 | notbid 308 |
. . . . . . . . . . . . . 14
⊢ (𝑤 = 〈𝑦, 𝑧〉 → (¬ 𝑤 ∈ 𝑅 ↔ ¬ 𝑦𝑅𝑧)) |
83 | 78, 82 | imbi12d 334 |
. . . . . . . . . . . . 13
⊢ (𝑤 = 〈𝑦, 𝑧〉 → ((𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅) ↔ ((𝑦 = 𝑧 ∧ 𝑦 ∈ 𝐴) → ¬ 𝑦𝑅𝑧))) |
84 | 70, 83 | syl5ibrcom 237 |
. . . . . . . . . . . 12
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 = 〈𝑦, 𝑧〉 → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅))) |
85 | 84 | exlimdvv 1862 |
. . . . . . . . . . 11
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (∃𝑦∃𝑧 𝑤 = 〈𝑦, 𝑧〉 → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅))) |
86 | 85 | impd 447 |
. . . . . . . . . 10
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ((∃𝑦∃𝑧 𝑤 = 〈𝑦, 𝑧〉 ∧ 𝑤 ∈ ( I ↾ 𝐴)) → ¬ 𝑤 ∈ 𝑅)) |
87 | 58, 86 | syl5 34 |
. . . . . . . . 9
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ ( I ↾ 𝐴) → ¬ 𝑤 ∈ 𝑅)) |
88 | 87 | con2d 129 |
. . . . . . . 8
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → (𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴))) |
89 | 88 | alrimiv 1855 |
. . . . . . 7
⊢
(∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥) → ∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴))) |
90 | 54, 89 | impbii 199 |
. . . . . 6
⊢
(∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥)) |
91 | | df-ral 2917 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ¬ 𝑥𝑅𝑥 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ¬ 𝑥𝑅𝑥)) |
92 | 90, 91 | bitr4i 267 |
. . . . 5
⊢
(∀𝑤(𝑤 ∈ 𝑅 → ¬ 𝑤 ∈ ( I ↾ 𝐴)) ↔ ∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥) |
93 | 35, 36, 92 | 3bitri 286 |
. . . 4
⊢ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ↔
∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥) |
94 | | ralcom 3098 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
95 | | r19.23v 3023 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
96 | 95 | ralbii 2980 |
. . . . . . 7
⊢
(∀𝑧 ∈
𝐴 ∀𝑦 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
97 | 94, 96 | bitri 264 |
. . . . . 6
⊢
(∀𝑦 ∈
𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
98 | 97 | ralbii 2980 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥 ∈ 𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
99 | | brin 4704 |
. . . . . . . . . . . 12
⊢ (𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ↔ (𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦)) |
100 | | brin 4704 |
. . . . . . . . . . . 12
⊢ (𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧 ↔ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) |
101 | 99, 100 | anbi12i 733 |
. . . . . . . . . . 11
⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧))) |
102 | | an4 865 |
. . . . . . . . . . . 12
⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧))) |
103 | | ancom 466 |
. . . . . . . . . . . 12
⊢ (((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) ∧ (𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) |
104 | | ancom 466 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ↔ (𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴)) |
105 | 104 | anbi1i 731 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))) |
106 | | brxp 5147 |
. . . . . . . . . . . . . . 15
⊢ (𝑥(𝐴 × 𝐴)𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴)) |
107 | | brxp 5147 |
. . . . . . . . . . . . . . 15
⊢ (𝑦(𝐴 × 𝐴)𝑧 ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) |
108 | 106, 107 | anbi12i 733 |
. . . . . . . . . . . . . 14
⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))) |
109 | | anandi 871 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ↔ ((𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴) ∧ (𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))) |
110 | 105, 108,
109 | 3bitr4i 292 |
. . . . . . . . . . . . 13
⊢ ((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ↔ (𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴))) |
111 | 110 | anbi1i 731 |
. . . . . . . . . . . 12
⊢ (((𝑥(𝐴 × 𝐴)𝑦 ∧ 𝑦(𝐴 × 𝐴)𝑧) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) |
112 | 102, 103,
111 | 3bitri 286 |
. . . . . . . . . . 11
⊢ (((𝑥𝑅𝑦 ∧ 𝑥(𝐴 × 𝐴)𝑦) ∧ (𝑦𝑅𝑧 ∧ 𝑦(𝐴 × 𝐴)𝑧)) ↔ ((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) |
113 | | anass 681 |
. . . . . . . . . . 11
⊢ (((𝑦 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))) |
114 | 101, 112,
113 | 3bitri 286 |
. . . . . . . . . 10
⊢ ((𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ (𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))) |
115 | 114 | exbii 1774 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))) |
116 | 42, 72 | brco 5292 |
. . . . . . . . . 10
⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ ∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧)) |
117 | | df-br 4654 |
. . . . . . . . . 10
⊢ (𝑥((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))𝑧 ↔ 〈𝑥, 𝑧〉 ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))) |
118 | 116, 117 | bitr3i 266 |
. . . . . . . . 9
⊢
(∃𝑦(𝑥(𝑅 ∩ (𝐴 × 𝐴))𝑦 ∧ 𝑦(𝑅 ∩ (𝐴 × 𝐴))𝑧) ↔ 〈𝑥, 𝑧〉 ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))) |
119 | | df-rex 2918 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)))) |
120 | | r19.42v 3092 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
𝐴 ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) |
121 | 119, 120 | bitr3i 266 |
. . . . . . . . 9
⊢
(∃𝑦(𝑦 ∈ 𝐴 ∧ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧))) |
122 | 115, 118,
121 | 3bitr3ri 291 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) ↔ 〈𝑥, 𝑧〉 ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴)))) |
123 | | df-br 4654 |
. . . . . . . 8
⊢ (𝑥𝑅𝑧 ↔ 〈𝑥, 𝑧〉 ∈ 𝑅) |
124 | 122, 123 | imbi12i 340 |
. . . . . . 7
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ (〈𝑥, 𝑧〉 ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → 〈𝑥, 𝑧〉 ∈ 𝑅)) |
125 | 124 | 2albii 1748 |
. . . . . 6
⊢
(∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(〈𝑥, 𝑧〉 ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → 〈𝑥, 𝑧〉 ∈ 𝑅)) |
126 | | r2al 2939 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
127 | | impexp 462 |
. . . . . . . 8
⊢ ((((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
128 | 127 | 2albii 1748 |
. . . . . . 7
⊢
(∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) → (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
129 | 126, 128 | bitr4i 267 |
. . . . . 6
⊢
(∀𝑥 ∈
𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ∀𝑥∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ ∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧)) → 𝑥𝑅𝑧)) |
130 | | relco 5633 |
. . . . . . 7
⊢ Rel
((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) |
131 | | ssrel 5207 |
. . . . . . 7
⊢ (Rel
((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(〈𝑥, 𝑧〉 ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → 〈𝑥, 𝑧〉 ∈ 𝑅))) |
132 | 130, 131 | ax-mp 5 |
. . . . . 6
⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥∀𝑧(〈𝑥, 𝑧〉 ∈ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) → 〈𝑥, 𝑧〉 ∈ 𝑅)) |
133 | 125, 129,
132 | 3bitr4i 292 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 ∀𝑧 ∈ 𝐴 (∃𝑦 ∈ 𝐴 (𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧) ↔ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) |
134 | 98, 133 | bitr2i 265 |
. . . 4
⊢ (((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅 ↔ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧)) |
135 | 93, 134 | anbi12i 733 |
. . 3
⊢ (((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅) ↔ (∀𝑥 ∈ 𝐴 ¬ 𝑥𝑅𝑥 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∀𝑧 ∈ 𝐴 ((𝑥𝑅𝑦 ∧ 𝑦𝑅𝑧) → 𝑥𝑅𝑧))) |
136 | 33, 34, 135 | 3bitr4g 303 |
. 2
⊢ (𝐴 ≠ ∅ → (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅))) |
137 | 26, 136 | pm2.61ine 2877 |
1
⊢ (𝑅 Po 𝐴 ↔ ((𝑅 ∩ ( I ↾ 𝐴)) = ∅ ∧ ((𝑅 ∩ (𝐴 × 𝐴)) ∘ (𝑅 ∩ (𝐴 × 𝐴))) ⊆ 𝑅)) |