Step |
Hyp |
Ref |
Expression |
1 |
|
pofun.1 |
⊢ 𝑆 = { 〈 𝑥 , 𝑦 〉 ∣ 𝑋 𝑅 𝑌 } |
2 |
|
pofun.2 |
⊢ ( 𝑥 = 𝑦 → 𝑋 = 𝑌 ) |
3 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 |
4 |
3
|
nfel1 |
⊢ Ⅎ 𝑥 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 |
5 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑣 → 𝑋 = ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ) |
6 |
5
|
eleq1d |
⊢ ( 𝑥 = 𝑣 → ( 𝑋 ∈ 𝐵 ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
7 |
4 6
|
rspc |
⊢ ( 𝑣 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
8 |
7
|
impcom |
⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ) → ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) |
9 |
|
poirr |
⊢ ( ( 𝑅 Po 𝐵 ∧ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) → ¬ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ) |
10 |
|
df-br |
⊢ ( 𝑣 𝑆 𝑣 ↔ 〈 𝑣 , 𝑣 〉 ∈ 𝑆 ) |
11 |
1
|
eleq2i |
⊢ ( 〈 𝑣 , 𝑣 〉 ∈ 𝑆 ↔ 〈 𝑣 , 𝑣 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑋 𝑅 𝑌 } ) |
12 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑅 |
13 |
|
nfcv |
⊢ Ⅎ 𝑥 𝑌 |
14 |
3 12 13
|
nfbr |
⊢ Ⅎ 𝑥 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 𝑌 |
15 |
|
nfv |
⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 |
16 |
|
vex |
⊢ 𝑣 ∈ V |
17 |
5
|
breq1d |
⊢ ( 𝑥 = 𝑣 → ( 𝑋 𝑅 𝑌 ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 𝑌 ) ) |
18 |
|
vex |
⊢ 𝑦 ∈ V |
19 |
18 2
|
csbie |
⊢ ⦋ 𝑦 / 𝑥 ⦌ 𝑋 = 𝑌 |
20 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑣 → ⦋ 𝑦 / 𝑥 ⦌ 𝑋 = ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ) |
21 |
19 20
|
eqtr3id |
⊢ ( 𝑦 = 𝑣 → 𝑌 = ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ) |
22 |
21
|
breq2d |
⊢ ( 𝑦 = 𝑣 → ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 𝑌 ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ) ) |
23 |
14 15 16 16 17 22
|
opelopabf |
⊢ ( 〈 𝑣 , 𝑣 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑋 𝑅 𝑌 } ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ) |
24 |
10 11 23
|
3bitri |
⊢ ( 𝑣 𝑆 𝑣 ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ) |
25 |
9 24
|
sylnibr |
⊢ ( ( 𝑅 Po 𝐵 ∧ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) → ¬ 𝑣 𝑆 𝑣 ) |
26 |
8 25
|
sylan2 |
⊢ ( ( 𝑅 Po 𝐵 ∧ ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ 𝑣 ∈ 𝐴 ) ) → ¬ 𝑣 𝑆 𝑣 ) |
27 |
26
|
anassrs |
⊢ ( ( ( 𝑅 Po 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ) ∧ 𝑣 ∈ 𝐴 ) → ¬ 𝑣 𝑆 𝑣 ) |
28 |
7
|
com12 |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ( 𝑣 ∈ 𝐴 → ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
29 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 |
30 |
29
|
nfel1 |
⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 |
31 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑤 → 𝑋 = ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ) |
32 |
31
|
eleq1d |
⊢ ( 𝑥 = 𝑤 → ( 𝑋 ∈ 𝐵 ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
33 |
30 32
|
rspc |
⊢ ( 𝑤 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
34 |
33
|
com12 |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ( 𝑤 ∈ 𝐴 → ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
35 |
|
nfcsb1v |
⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 |
36 |
35
|
nfel1 |
⊢ Ⅎ 𝑥 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 |
37 |
|
csbeq1a |
⊢ ( 𝑥 = 𝑧 → 𝑋 = ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) |
38 |
37
|
eleq1d |
⊢ ( 𝑥 = 𝑧 → ( 𝑋 ∈ 𝐵 ↔ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
39 |
36 38
|
rspc |
⊢ ( 𝑧 ∈ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
40 |
39
|
com12 |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ( 𝑧 ∈ 𝐴 → ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
41 |
28 34 40
|
3anim123d |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 → ( ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) ) |
42 |
41
|
imp |
⊢ ( ( ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
43 |
42
|
adantll |
⊢ ( ( ( 𝑅 Po 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) |
44 |
|
potr |
⊢ ( ( 𝑅 Po 𝐵 ∧ ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) → ( ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) → ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) ) |
45 |
|
df-br |
⊢ ( 𝑣 𝑆 𝑤 ↔ 〈 𝑣 , 𝑤 〉 ∈ 𝑆 ) |
46 |
1
|
eleq2i |
⊢ ( 〈 𝑣 , 𝑤 〉 ∈ 𝑆 ↔ 〈 𝑣 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑋 𝑅 𝑌 } ) |
47 |
|
nfv |
⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 |
48 |
|
vex |
⊢ 𝑤 ∈ V |
49 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑤 → ⦋ 𝑦 / 𝑥 ⦌ 𝑋 = ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ) |
50 |
19 49
|
eqtr3id |
⊢ ( 𝑦 = 𝑤 → 𝑌 = ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ) |
51 |
50
|
breq2d |
⊢ ( 𝑦 = 𝑤 → ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 𝑌 ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ) ) |
52 |
14 47 16 48 17 51
|
opelopabf |
⊢ ( 〈 𝑣 , 𝑤 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑋 𝑅 𝑌 } ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ) |
53 |
45 46 52
|
3bitri |
⊢ ( 𝑣 𝑆 𝑤 ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ) |
54 |
|
df-br |
⊢ ( 𝑤 𝑆 𝑧 ↔ 〈 𝑤 , 𝑧 〉 ∈ 𝑆 ) |
55 |
1
|
eleq2i |
⊢ ( 〈 𝑤 , 𝑧 〉 ∈ 𝑆 ↔ 〈 𝑤 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑋 𝑅 𝑌 } ) |
56 |
29 12 13
|
nfbr |
⊢ Ⅎ 𝑥 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 𝑅 𝑌 |
57 |
|
nfv |
⊢ Ⅎ 𝑦 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 |
58 |
|
vex |
⊢ 𝑧 ∈ V |
59 |
31
|
breq1d |
⊢ ( 𝑥 = 𝑤 → ( 𝑋 𝑅 𝑌 ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 𝑅 𝑌 ) ) |
60 |
|
csbeq1 |
⊢ ( 𝑦 = 𝑧 → ⦋ 𝑦 / 𝑥 ⦌ 𝑋 = ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) |
61 |
19 60
|
eqtr3id |
⊢ ( 𝑦 = 𝑧 → 𝑌 = ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) |
62 |
61
|
breq2d |
⊢ ( 𝑦 = 𝑧 → ( ⦋ 𝑤 / 𝑥 ⦌ 𝑋 𝑅 𝑌 ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) ) |
63 |
56 57 48 58 59 62
|
opelopabf |
⊢ ( 〈 𝑤 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑋 𝑅 𝑌 } ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) |
64 |
54 55 63
|
3bitri |
⊢ ( 𝑤 𝑆 𝑧 ↔ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) |
65 |
53 64
|
anbi12i |
⊢ ( ( 𝑣 𝑆 𝑤 ∧ 𝑤 𝑆 𝑧 ) ↔ ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) ) |
66 |
|
df-br |
⊢ ( 𝑣 𝑆 𝑧 ↔ 〈 𝑣 , 𝑧 〉 ∈ 𝑆 ) |
67 |
1
|
eleq2i |
⊢ ( 〈 𝑣 , 𝑧 〉 ∈ 𝑆 ↔ 〈 𝑣 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑋 𝑅 𝑌 } ) |
68 |
|
nfv |
⊢ Ⅎ 𝑦 ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 |
69 |
61
|
breq2d |
⊢ ( 𝑦 = 𝑧 → ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 𝑌 ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) ) |
70 |
14 68 16 58 17 69
|
opelopabf |
⊢ ( 〈 𝑣 , 𝑧 〉 ∈ { 〈 𝑥 , 𝑦 〉 ∣ 𝑋 𝑅 𝑌 } ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) |
71 |
66 67 70
|
3bitri |
⊢ ( 𝑣 𝑆 𝑧 ↔ ⦋ 𝑣 / 𝑥 ⦌ 𝑋 𝑅 ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ) |
72 |
44 65 71
|
3imtr4g |
⊢ ( ( 𝑅 Po 𝐵 ∧ ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑣 𝑆 𝑤 ∧ 𝑤 𝑆 𝑧 ) → 𝑣 𝑆 𝑧 ) ) |
73 |
72
|
adantlr |
⊢ ( ( ( 𝑅 Po 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ) ∧ ( ⦋ 𝑣 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑤 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ∧ ⦋ 𝑧 / 𝑥 ⦌ 𝑋 ∈ 𝐵 ) ) → ( ( 𝑣 𝑆 𝑤 ∧ 𝑤 𝑆 𝑧 ) → 𝑣 𝑆 𝑧 ) ) |
74 |
43 73
|
syldan |
⊢ ( ( ( 𝑅 Po 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ) ∧ ( 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) ) → ( ( 𝑣 𝑆 𝑤 ∧ 𝑤 𝑆 𝑧 ) → 𝑣 𝑆 𝑧 ) ) |
75 |
27 74
|
ispod |
⊢ ( ( 𝑅 Po 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝑋 ∈ 𝐵 ) → 𝑆 Po 𝐴 ) |