Step |
Hyp |
Ref |
Expression |
1 |
|
pofun.1 |
|- S = { <. x , y >. | X R Y } |
2 |
|
pofun.2 |
|- ( x = y -> X = Y ) |
3 |
|
nfcsb1v |
|- F/_ x [_ v / x ]_ X |
4 |
3
|
nfel1 |
|- F/ x [_ v / x ]_ X e. B |
5 |
|
csbeq1a |
|- ( x = v -> X = [_ v / x ]_ X ) |
6 |
5
|
eleq1d |
|- ( x = v -> ( X e. B <-> [_ v / x ]_ X e. B ) ) |
7 |
4 6
|
rspc |
|- ( v e. A -> ( A. x e. A X e. B -> [_ v / x ]_ X e. B ) ) |
8 |
7
|
impcom |
|- ( ( A. x e. A X e. B /\ v e. A ) -> [_ v / x ]_ X e. B ) |
9 |
|
poirr |
|- ( ( R Po B /\ [_ v / x ]_ X e. B ) -> -. [_ v / x ]_ X R [_ v / x ]_ X ) |
10 |
|
df-br |
|- ( v S v <-> <. v , v >. e. S ) |
11 |
1
|
eleq2i |
|- ( <. v , v >. e. S <-> <. v , v >. e. { <. x , y >. | X R Y } ) |
12 |
|
nfcv |
|- F/_ x R |
13 |
|
nfcv |
|- F/_ x Y |
14 |
3 12 13
|
nfbr |
|- F/ x [_ v / x ]_ X R Y |
15 |
|
nfv |
|- F/ y [_ v / x ]_ X R [_ v / x ]_ X |
16 |
|
vex |
|- v e. _V |
17 |
5
|
breq1d |
|- ( x = v -> ( X R Y <-> [_ v / x ]_ X R Y ) ) |
18 |
|
vex |
|- y e. _V |
19 |
18 2
|
csbie |
|- [_ y / x ]_ X = Y |
20 |
|
csbeq1 |
|- ( y = v -> [_ y / x ]_ X = [_ v / x ]_ X ) |
21 |
19 20
|
eqtr3id |
|- ( y = v -> Y = [_ v / x ]_ X ) |
22 |
21
|
breq2d |
|- ( y = v -> ( [_ v / x ]_ X R Y <-> [_ v / x ]_ X R [_ v / x ]_ X ) ) |
23 |
14 15 16 16 17 22
|
opelopabf |
|- ( <. v , v >. e. { <. x , y >. | X R Y } <-> [_ v / x ]_ X R [_ v / x ]_ X ) |
24 |
10 11 23
|
3bitri |
|- ( v S v <-> [_ v / x ]_ X R [_ v / x ]_ X ) |
25 |
9 24
|
sylnibr |
|- ( ( R Po B /\ [_ v / x ]_ X e. B ) -> -. v S v ) |
26 |
8 25
|
sylan2 |
|- ( ( R Po B /\ ( A. x e. A X e. B /\ v e. A ) ) -> -. v S v ) |
27 |
26
|
anassrs |
|- ( ( ( R Po B /\ A. x e. A X e. B ) /\ v e. A ) -> -. v S v ) |
28 |
7
|
com12 |
|- ( A. x e. A X e. B -> ( v e. A -> [_ v / x ]_ X e. B ) ) |
29 |
|
nfcsb1v |
|- F/_ x [_ w / x ]_ X |
30 |
29
|
nfel1 |
|- F/ x [_ w / x ]_ X e. B |
31 |
|
csbeq1a |
|- ( x = w -> X = [_ w / x ]_ X ) |
32 |
31
|
eleq1d |
|- ( x = w -> ( X e. B <-> [_ w / x ]_ X e. B ) ) |
33 |
30 32
|
rspc |
|- ( w e. A -> ( A. x e. A X e. B -> [_ w / x ]_ X e. B ) ) |
34 |
33
|
com12 |
|- ( A. x e. A X e. B -> ( w e. A -> [_ w / x ]_ X e. B ) ) |
35 |
|
nfcsb1v |
|- F/_ x [_ z / x ]_ X |
36 |
35
|
nfel1 |
|- F/ x [_ z / x ]_ X e. B |
37 |
|
csbeq1a |
|- ( x = z -> X = [_ z / x ]_ X ) |
38 |
37
|
eleq1d |
|- ( x = z -> ( X e. B <-> [_ z / x ]_ X e. B ) ) |
39 |
36 38
|
rspc |
|- ( z e. A -> ( A. x e. A X e. B -> [_ z / x ]_ X e. B ) ) |
40 |
39
|
com12 |
|- ( A. x e. A X e. B -> ( z e. A -> [_ z / x ]_ X e. B ) ) |
41 |
28 34 40
|
3anim123d |
|- ( A. x e. A X e. B -> ( ( v e. A /\ w e. A /\ z e. A ) -> ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) ) |
42 |
41
|
imp |
|- ( ( A. x e. A X e. B /\ ( v e. A /\ w e. A /\ z e. A ) ) -> ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) |
43 |
42
|
adantll |
|- ( ( ( R Po B /\ A. x e. A X e. B ) /\ ( v e. A /\ w e. A /\ z e. A ) ) -> ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) |
44 |
|
potr |
|- ( ( R Po B /\ ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) -> ( ( [_ v / x ]_ X R [_ w / x ]_ X /\ [_ w / x ]_ X R [_ z / x ]_ X ) -> [_ v / x ]_ X R [_ z / x ]_ X ) ) |
45 |
|
df-br |
|- ( v S w <-> <. v , w >. e. S ) |
46 |
1
|
eleq2i |
|- ( <. v , w >. e. S <-> <. v , w >. e. { <. x , y >. | X R Y } ) |
47 |
|
nfv |
|- F/ y [_ v / x ]_ X R [_ w / x ]_ X |
48 |
|
vex |
|- w e. _V |
49 |
|
csbeq1 |
|- ( y = w -> [_ y / x ]_ X = [_ w / x ]_ X ) |
50 |
19 49
|
eqtr3id |
|- ( y = w -> Y = [_ w / x ]_ X ) |
51 |
50
|
breq2d |
|- ( y = w -> ( [_ v / x ]_ X R Y <-> [_ v / x ]_ X R [_ w / x ]_ X ) ) |
52 |
14 47 16 48 17 51
|
opelopabf |
|- ( <. v , w >. e. { <. x , y >. | X R Y } <-> [_ v / x ]_ X R [_ w / x ]_ X ) |
53 |
45 46 52
|
3bitri |
|- ( v S w <-> [_ v / x ]_ X R [_ w / x ]_ X ) |
54 |
|
df-br |
|- ( w S z <-> <. w , z >. e. S ) |
55 |
1
|
eleq2i |
|- ( <. w , z >. e. S <-> <. w , z >. e. { <. x , y >. | X R Y } ) |
56 |
29 12 13
|
nfbr |
|- F/ x [_ w / x ]_ X R Y |
57 |
|
nfv |
|- F/ y [_ w / x ]_ X R [_ z / x ]_ X |
58 |
|
vex |
|- z e. _V |
59 |
31
|
breq1d |
|- ( x = w -> ( X R Y <-> [_ w / x ]_ X R Y ) ) |
60 |
|
csbeq1 |
|- ( y = z -> [_ y / x ]_ X = [_ z / x ]_ X ) |
61 |
19 60
|
eqtr3id |
|- ( y = z -> Y = [_ z / x ]_ X ) |
62 |
61
|
breq2d |
|- ( y = z -> ( [_ w / x ]_ X R Y <-> [_ w / x ]_ X R [_ z / x ]_ X ) ) |
63 |
56 57 48 58 59 62
|
opelopabf |
|- ( <. w , z >. e. { <. x , y >. | X R Y } <-> [_ w / x ]_ X R [_ z / x ]_ X ) |
64 |
54 55 63
|
3bitri |
|- ( w S z <-> [_ w / x ]_ X R [_ z / x ]_ X ) |
65 |
53 64
|
anbi12i |
|- ( ( v S w /\ w S z ) <-> ( [_ v / x ]_ X R [_ w / x ]_ X /\ [_ w / x ]_ X R [_ z / x ]_ X ) ) |
66 |
|
df-br |
|- ( v S z <-> <. v , z >. e. S ) |
67 |
1
|
eleq2i |
|- ( <. v , z >. e. S <-> <. v , z >. e. { <. x , y >. | X R Y } ) |
68 |
|
nfv |
|- F/ y [_ v / x ]_ X R [_ z / x ]_ X |
69 |
61
|
breq2d |
|- ( y = z -> ( [_ v / x ]_ X R Y <-> [_ v / x ]_ X R [_ z / x ]_ X ) ) |
70 |
14 68 16 58 17 69
|
opelopabf |
|- ( <. v , z >. e. { <. x , y >. | X R Y } <-> [_ v / x ]_ X R [_ z / x ]_ X ) |
71 |
66 67 70
|
3bitri |
|- ( v S z <-> [_ v / x ]_ X R [_ z / x ]_ X ) |
72 |
44 65 71
|
3imtr4g |
|- ( ( R Po B /\ ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) -> ( ( v S w /\ w S z ) -> v S z ) ) |
73 |
72
|
adantlr |
|- ( ( ( R Po B /\ A. x e. A X e. B ) /\ ( [_ v / x ]_ X e. B /\ [_ w / x ]_ X e. B /\ [_ z / x ]_ X e. B ) ) -> ( ( v S w /\ w S z ) -> v S z ) ) |
74 |
43 73
|
syldan |
|- ( ( ( R Po B /\ A. x e. A X e. B ) /\ ( v e. A /\ w e. A /\ z e. A ) ) -> ( ( v S w /\ w S z ) -> v S z ) ) |
75 |
27 74
|
ispod |
|- ( ( R Po B /\ A. x e. A X e. B ) -> S Po A ) |