Step | Hyp | Ref
| Expression |
1 | | nfcsb1v 2876 |
. . . . . . 7
⊢
Ⅎx⦋v / x⦌𝑋 |
2 | 1 | nfel1 2185 |
. . . . . 6
⊢
Ⅎx⦋v / x⦌𝑋 ∈
B |
3 | | csbeq1a 2854 |
. . . . . . 7
⊢ (x = v →
𝑋 = ⦋v / x⦌𝑋) |
4 | 3 | eleq1d 2103 |
. . . . . 6
⊢ (x = v →
(𝑋 ∈ B ↔
⦋v / x⦌𝑋 ∈
B)) |
5 | 2, 4 | rspc 2644 |
. . . . 5
⊢ (v ∈ A → (∀x ∈ A 𝑋 ∈ B →
⦋v / x⦌𝑋 ∈
B)) |
6 | 5 | impcom 116 |
. . . 4
⊢ ((∀x ∈ A 𝑋 ∈ B ∧ v ∈ A) →
⦋v / x⦌𝑋 ∈
B) |
7 | | poirr 4035 |
. . . . 5
⊢ ((𝑅 Po B ∧
⦋v / x⦌𝑋 ∈
B) → ¬ ⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋) |
8 | | df-br 3756 |
. . . . . 6
⊢ (v𝑆v ↔
〈v, v〉 ∈ 𝑆) |
9 | | pofun.1 |
. . . . . . 7
⊢ 𝑆 = {〈x, y〉
∣ 𝑋𝑅𝑌} |
10 | 9 | eleq2i 2101 |
. . . . . 6
⊢
(〈v, v〉 ∈ 𝑆 ↔ 〈v, v〉 ∈ {〈x,
y〉 ∣ 𝑋𝑅𝑌}) |
11 | | nfcv 2175 |
. . . . . . . 8
⊢
Ⅎx𝑅 |
12 | | nfcv 2175 |
. . . . . . . 8
⊢
Ⅎx𝑌 |
13 | 1, 11, 12 | nfbr 3799 |
. . . . . . 7
⊢
Ⅎx⦋v / x⦌𝑋𝑅𝑌 |
14 | | nfv 1418 |
. . . . . . 7
⊢
Ⅎy⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋 |
15 | | vex 2554 |
. . . . . . 7
⊢ v ∈
V |
16 | 3 | breq1d 3765 |
. . . . . . 7
⊢ (x = v →
(𝑋𝑅𝑌 ↔ ⦋v / x⦌𝑋𝑅𝑌)) |
17 | | vex 2554 |
. . . . . . . . . 10
⊢ y ∈
V |
18 | | pofun.2 |
. . . . . . . . . 10
⊢ (x = y →
𝑋 = 𝑌) |
19 | 17, 12, 18 | csbief 2885 |
. . . . . . . . 9
⊢
⦋y / x⦌𝑋 = 𝑌 |
20 | | csbeq1 2849 |
. . . . . . . . 9
⊢ (y = v →
⦋y / x⦌𝑋 = ⦋v / x⦌𝑋) |
21 | 19, 20 | syl5eqr 2083 |
. . . . . . . 8
⊢ (y = v →
𝑌 = ⦋v / x⦌𝑋) |
22 | 21 | breq2d 3767 |
. . . . . . 7
⊢ (y = v →
(⦋v / x⦌𝑋𝑅𝑌 ↔ ⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋)) |
23 | 13, 14, 15, 15, 16, 22 | opelopabf 4002 |
. . . . . 6
⊢
(〈v, v〉 ∈
{〈x, y〉 ∣ 𝑋𝑅𝑌} ↔ ⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋) |
24 | 8, 10, 23 | 3bitri 195 |
. . . . 5
⊢ (v𝑆v ↔
⦋v / x⦌𝑋𝑅⦋v / x⦌𝑋) |
25 | 7, 24 | sylnibr 601 |
. . . 4
⊢ ((𝑅 Po B ∧
⦋v / x⦌𝑋 ∈
B) → ¬ v𝑆v) |
26 | 6, 25 | sylan2 270 |
. . 3
⊢ ((𝑅 Po B ∧ (∀x ∈ A 𝑋 ∈ B ∧ v ∈ A)) →
¬ v𝑆v) |
27 | 26 | anassrs 380 |
. 2
⊢ (((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) ∧ v ∈ A) →
¬ v𝑆v) |
28 | 5 | com12 27 |
. . . . . 6
⊢ (∀x ∈ A 𝑋 ∈ B →
(v ∈
A → ⦋v / x⦌𝑋 ∈
B)) |
29 | | nfcsb1v 2876 |
. . . . . . . . 9
⊢
Ⅎx⦋w / x⦌𝑋 |
30 | 29 | nfel1 2185 |
. . . . . . . 8
⊢
Ⅎx⦋w / x⦌𝑋 ∈
B |
31 | | csbeq1a 2854 |
. . . . . . . . 9
⊢ (x = w →
𝑋 = ⦋w / x⦌𝑋) |
32 | 31 | eleq1d 2103 |
. . . . . . . 8
⊢ (x = w →
(𝑋 ∈ B ↔
⦋w / x⦌𝑋 ∈
B)) |
33 | 30, 32 | rspc 2644 |
. . . . . . 7
⊢ (w ∈ A → (∀x ∈ A 𝑋 ∈ B →
⦋w / x⦌𝑋 ∈
B)) |
34 | 33 | com12 27 |
. . . . . 6
⊢ (∀x ∈ A 𝑋 ∈ B →
(w ∈
A → ⦋w / x⦌𝑋 ∈
B)) |
35 | | nfcsb1v 2876 |
. . . . . . . . 9
⊢
Ⅎx⦋z / x⦌𝑋 |
36 | 35 | nfel1 2185 |
. . . . . . . 8
⊢
Ⅎx⦋z / x⦌𝑋 ∈
B |
37 | | csbeq1a 2854 |
. . . . . . . . 9
⊢ (x = z →
𝑋 = ⦋z / x⦌𝑋) |
38 | 37 | eleq1d 2103 |
. . . . . . . 8
⊢ (x = z →
(𝑋 ∈ B ↔
⦋z / x⦌𝑋 ∈
B)) |
39 | 36, 38 | rspc 2644 |
. . . . . . 7
⊢ (z ∈ A → (∀x ∈ A 𝑋 ∈ B →
⦋z / x⦌𝑋 ∈
B)) |
40 | 39 | com12 27 |
. . . . . 6
⊢ (∀x ∈ A 𝑋 ∈ B →
(z ∈
A → ⦋z / x⦌𝑋 ∈
B)) |
41 | 28, 34, 40 | 3anim123d 1213 |
. . . . 5
⊢ (∀x ∈ A 𝑋 ∈ B →
((v ∈
A ∧
w ∈
A ∧
z ∈
A) → (⦋v / x⦌𝑋 ∈
B ∧
⦋w / x⦌𝑋 ∈
B ∧
⦋z / x⦌𝑋 ∈
B))) |
42 | 41 | imp 115 |
. . . 4
⊢ ((∀x ∈ A 𝑋 ∈ B ∧ (v ∈ A ∧ w ∈ A ∧ z ∈ A)) →
(⦋v / x⦌𝑋 ∈
B ∧
⦋w / x⦌𝑋 ∈
B ∧
⦋z / x⦌𝑋 ∈
B)) |
43 | 42 | adantll 445 |
. . 3
⊢ (((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) ∧ (v ∈ A ∧ w ∈ A ∧ z ∈ A)) →
(⦋v / x⦌𝑋 ∈
B ∧
⦋w / x⦌𝑋 ∈
B ∧
⦋z / x⦌𝑋 ∈
B)) |
44 | | potr 4036 |
. . . . 5
⊢ ((𝑅 Po B ∧
(⦋v / x⦌𝑋 ∈
B ∧
⦋w / x⦌𝑋 ∈
B ∧
⦋z / x⦌𝑋 ∈
B)) → ((⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋 ∧
⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋) → ⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋)) |
45 | | df-br 3756 |
. . . . . . 7
⊢ (v𝑆w ↔
〈v, w〉 ∈ 𝑆) |
46 | 9 | eleq2i 2101 |
. . . . . . 7
⊢
(〈v, w〉 ∈ 𝑆 ↔ 〈v, w〉 ∈ {〈x,
y〉 ∣ 𝑋𝑅𝑌}) |
47 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎy⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋 |
48 | | vex 2554 |
. . . . . . . 8
⊢ w ∈
V |
49 | | csbeq1 2849 |
. . . . . . . . . 10
⊢ (y = w →
⦋y / x⦌𝑋 = ⦋w / x⦌𝑋) |
50 | 19, 49 | syl5eqr 2083 |
. . . . . . . . 9
⊢ (y = w →
𝑌 = ⦋w / x⦌𝑋) |
51 | 50 | breq2d 3767 |
. . . . . . . 8
⊢ (y = w →
(⦋v / x⦌𝑋𝑅𝑌 ↔ ⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋)) |
52 | 13, 47, 15, 48, 16, 51 | opelopabf 4002 |
. . . . . . 7
⊢
(〈v, w〉 ∈
{〈x, y〉 ∣ 𝑋𝑅𝑌} ↔ ⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋) |
53 | 45, 46, 52 | 3bitri 195 |
. . . . . 6
⊢ (v𝑆w ↔
⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋) |
54 | | df-br 3756 |
. . . . . . 7
⊢ (w𝑆z ↔
〈w, z〉 ∈ 𝑆) |
55 | 9 | eleq2i 2101 |
. . . . . . 7
⊢
(〈w, z〉 ∈ 𝑆 ↔ 〈w, z〉 ∈ {〈x,
y〉 ∣ 𝑋𝑅𝑌}) |
56 | 29, 11, 12 | nfbr 3799 |
. . . . . . . 8
⊢
Ⅎx⦋w / x⦌𝑋𝑅𝑌 |
57 | | nfv 1418 |
. . . . . . . 8
⊢
Ⅎy⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋 |
58 | | vex 2554 |
. . . . . . . 8
⊢ z ∈
V |
59 | 31 | breq1d 3765 |
. . . . . . . 8
⊢ (x = w →
(𝑋𝑅𝑌 ↔ ⦋w / x⦌𝑋𝑅𝑌)) |
60 | | csbeq1 2849 |
. . . . . . . . . 10
⊢ (y = z →
⦋y / x⦌𝑋 = ⦋z / x⦌𝑋) |
61 | 19, 60 | syl5eqr 2083 |
. . . . . . . . 9
⊢ (y = z →
𝑌 = ⦋z / x⦌𝑋) |
62 | 61 | breq2d 3767 |
. . . . . . . 8
⊢ (y = z →
(⦋w / x⦌𝑋𝑅𝑌 ↔ ⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋)) |
63 | 56, 57, 48, 58, 59, 62 | opelopabf 4002 |
. . . . . . 7
⊢
(〈w, z〉 ∈
{〈x, y〉 ∣ 𝑋𝑅𝑌} ↔ ⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋) |
64 | 54, 55, 63 | 3bitri 195 |
. . . . . 6
⊢ (w𝑆z ↔
⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋) |
65 | 53, 64 | anbi12i 433 |
. . . . 5
⊢
((v𝑆w ∧ w𝑆z) ↔ (⦋v / x⦌𝑋𝑅⦋w / x⦌𝑋 ∧
⦋w / x⦌𝑋𝑅⦋z / x⦌𝑋)) |
66 | | df-br 3756 |
. . . . . 6
⊢ (v𝑆z ↔
〈v, z〉 ∈ 𝑆) |
67 | 9 | eleq2i 2101 |
. . . . . 6
⊢
(〈v, z〉 ∈ 𝑆 ↔ 〈v, z〉 ∈ {〈x,
y〉 ∣ 𝑋𝑅𝑌}) |
68 | | nfv 1418 |
. . . . . . 7
⊢
Ⅎy⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋 |
69 | 61 | breq2d 3767 |
. . . . . . 7
⊢ (y = z →
(⦋v / x⦌𝑋𝑅𝑌 ↔ ⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋)) |
70 | 13, 68, 15, 58, 16, 69 | opelopabf 4002 |
. . . . . 6
⊢
(〈v, z〉 ∈
{〈x, y〉 ∣ 𝑋𝑅𝑌} ↔ ⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋) |
71 | 66, 67, 70 | 3bitri 195 |
. . . . 5
⊢ (v𝑆z ↔
⦋v / x⦌𝑋𝑅⦋z / x⦌𝑋) |
72 | 44, 65, 71 | 3imtr4g 194 |
. . . 4
⊢ ((𝑅 Po B ∧
(⦋v / x⦌𝑋 ∈
B ∧
⦋w / x⦌𝑋 ∈
B ∧
⦋z / x⦌𝑋 ∈
B)) → ((v𝑆w ∧ w𝑆z) → v𝑆z)) |
73 | 72 | adantlr 446 |
. . 3
⊢ (((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) ∧ (⦋v / x⦌𝑋 ∈
B ∧
⦋w / x⦌𝑋 ∈
B ∧
⦋z / x⦌𝑋 ∈
B)) → ((v𝑆w ∧ w𝑆z) → v𝑆z)) |
74 | 43, 73 | syldan 266 |
. 2
⊢ (((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) ∧ (v ∈ A ∧ w ∈ A ∧ z ∈ A)) →
((v𝑆w ∧ w𝑆z) → v𝑆z)) |
75 | 27, 74 | ispod 4032 |
1
⊢ ((𝑅 Po B ∧ ∀x ∈ A 𝑋 ∈ B) →
𝑆 Po A) |