Step |
Hyp |
Ref |
Expression |
1 |
|
breq2 |
|- ( t = s -> ( x R t <-> x R s ) ) |
2 |
1
|
cbvexvw |
|- ( E. t x R t <-> E. s x R s ) |
3 |
|
breq2 |
|- ( s = Z -> ( x R s <-> x R Z ) ) |
4 |
3
|
anbi1d |
|- ( s = Z -> ( ( x R s /\ ( x R t <-> t =/= Z ) ) <-> ( x R Z /\ ( x R t <-> t =/= Z ) ) ) ) |
5 |
|
bianir |
|- ( ( t =/= Z /\ ( x R t <-> t =/= Z ) ) -> x R t ) |
6 |
|
vex |
|- t e. _V |
7 |
|
breq2 |
|- ( y = t -> ( x R y <-> x R t ) ) |
8 |
|
neeq1 |
|- ( y = t -> ( y =/= Z <-> t =/= Z ) ) |
9 |
7 8
|
anbi12d |
|- ( y = t -> ( ( x R y /\ y =/= Z ) <-> ( x R t /\ t =/= Z ) ) ) |
10 |
6 9
|
spcev |
|- ( ( x R t /\ t =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) |
11 |
10
|
ex |
|- ( x R t -> ( t =/= Z -> E. y ( x R y /\ y =/= Z ) ) ) |
12 |
5 11
|
syl |
|- ( ( t =/= Z /\ ( x R t <-> t =/= Z ) ) -> ( t =/= Z -> E. y ( x R y /\ y =/= Z ) ) ) |
13 |
12
|
ex |
|- ( t =/= Z -> ( ( x R t <-> t =/= Z ) -> ( t =/= Z -> E. y ( x R y /\ y =/= Z ) ) ) ) |
14 |
13
|
pm2.43a |
|- ( t =/= Z -> ( ( x R t <-> t =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) ) |
15 |
14
|
adantld |
|- ( t =/= Z -> ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) ) |
16 |
|
nne |
|- ( -. t =/= Z <-> t = Z ) |
17 |
|
notbi |
|- ( ( x R t <-> t =/= Z ) <-> ( -. x R t <-> -. t =/= Z ) ) |
18 |
|
bianir |
|- ( ( -. t =/= Z /\ ( -. x R t <-> -. t =/= Z ) ) -> -. x R t ) |
19 |
|
breq2 |
|- ( Z = t -> ( x R Z <-> x R t ) ) |
20 |
19
|
eqcoms |
|- ( t = Z -> ( x R Z <-> x R t ) ) |
21 |
|
pm2.24 |
|- ( x R t -> ( -. x R t -> E. y ( x R y /\ y =/= Z ) ) ) |
22 |
20 21
|
syl6bi |
|- ( t = Z -> ( x R Z -> ( -. x R t -> E. y ( x R y /\ y =/= Z ) ) ) ) |
23 |
22
|
com13 |
|- ( -. x R t -> ( x R Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) ) |
24 |
18 23
|
syl |
|- ( ( -. t =/= Z /\ ( -. x R t <-> -. t =/= Z ) ) -> ( x R Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) ) |
25 |
24
|
ex |
|- ( -. t =/= Z -> ( ( -. x R t <-> -. t =/= Z ) -> ( x R Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) ) ) |
26 |
17 25
|
syl5bi |
|- ( -. t =/= Z -> ( ( x R t <-> t =/= Z ) -> ( x R Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) ) ) |
27 |
26
|
com13 |
|- ( x R Z -> ( ( x R t <-> t =/= Z ) -> ( -. t =/= Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) ) ) |
28 |
27
|
imp |
|- ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> ( -. t =/= Z -> ( t = Z -> E. y ( x R y /\ y =/= Z ) ) ) ) |
29 |
28
|
com13 |
|- ( t = Z -> ( -. t =/= Z -> ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) ) ) |
30 |
16 29
|
sylbi |
|- ( -. t =/= Z -> ( -. t =/= Z -> ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) ) ) |
31 |
30
|
pm2.43i |
|- ( -. t =/= Z -> ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) ) |
32 |
15 31
|
pm2.61i |
|- ( ( x R Z /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) |
33 |
4 32
|
syl6bi |
|- ( s = Z -> ( ( x R s /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) ) |
34 |
|
vex |
|- s e. _V |
35 |
|
breq2 |
|- ( y = s -> ( x R y <-> x R s ) ) |
36 |
|
neeq1 |
|- ( y = s -> ( y =/= Z <-> s =/= Z ) ) |
37 |
35 36
|
anbi12d |
|- ( y = s -> ( ( x R y /\ y =/= Z ) <-> ( x R s /\ s =/= Z ) ) ) |
38 |
34 37
|
spcev |
|- ( ( x R s /\ s =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) |
39 |
38
|
ex |
|- ( x R s -> ( s =/= Z -> E. y ( x R y /\ y =/= Z ) ) ) |
40 |
39
|
adantr |
|- ( ( x R s /\ ( x R t <-> t =/= Z ) ) -> ( s =/= Z -> E. y ( x R y /\ y =/= Z ) ) ) |
41 |
40
|
com12 |
|- ( s =/= Z -> ( ( x R s /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) ) |
42 |
33 41
|
pm2.61ine |
|- ( ( x R s /\ ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) |
43 |
42
|
expcom |
|- ( ( x R t <-> t =/= Z ) -> ( x R s -> E. y ( x R y /\ y =/= Z ) ) ) |
44 |
43
|
exlimiv |
|- ( E. t ( x R t <-> t =/= Z ) -> ( x R s -> E. y ( x R y /\ y =/= Z ) ) ) |
45 |
44
|
com12 |
|- ( x R s -> ( E. t ( x R t <-> t =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) ) |
46 |
45
|
exlimiv |
|- ( E. s x R s -> ( E. t ( x R t <-> t =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) ) |
47 |
2 46
|
sylbi |
|- ( E. t x R t -> ( E. t ( x R t <-> t =/= Z ) -> E. y ( x R y /\ y =/= Z ) ) ) |
48 |
47
|
imp |
|- ( ( E. t x R t /\ E. t ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) |
49 |
48
|
a1i |
|- ( ( R e. V /\ Z e. W ) -> ( ( E. t x R t /\ E. t ( x R t <-> t =/= Z ) ) -> E. y ( x R y /\ y =/= Z ) ) ) |
50 |
49
|
ss2abdv |
|- ( ( R e. V /\ Z e. W ) -> { x | ( E. t x R t /\ E. t ( x R t <-> t =/= Z ) ) } C_ { x | E. y ( x R y /\ y =/= Z ) } ) |
51 |
|
suppvalbr |
|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = { x | ( E. t x R t /\ E. t ( x R t <-> t =/= Z ) ) } ) |
52 |
|
cnvimadfsn |
|- ( `' R " ( _V \ { Z } ) ) = { x | E. y ( x R y /\ y =/= Z ) } |
53 |
52
|
a1i |
|- ( ( R e. V /\ Z e. W ) -> ( `' R " ( _V \ { Z } ) ) = { x | E. y ( x R y /\ y =/= Z ) } ) |
54 |
50 51 53
|
3sstr4d |
|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) C_ ( `' R " ( _V \ { Z } ) ) ) |
55 |
|
suppimacnvss |
|- ( ( R e. V /\ Z e. W ) -> ( `' R " ( _V \ { Z } ) ) C_ ( R supp Z ) ) |
56 |
54 55
|
eqssd |
|- ( ( R e. V /\ Z e. W ) -> ( R supp Z ) = ( `' R " ( _V \ { Z } ) ) ) |