Step |
Hyp |
Ref |
Expression |
1 |
|
reupr.a |
|- ( p = { a , b } -> ( ps <-> ch ) ) |
2 |
|
reupr.x |
|- ( p = { x , y } -> ( ps <-> th ) ) |
3 |
|
nfsbc1v |
|- F/ p [. q / p ]. ps |
4 |
|
nfsbc1v |
|- F/ p [. w / p ]. ps |
5 |
|
sbceq1a |
|- ( p = w -> ( ps <-> [. w / p ]. ps ) ) |
6 |
|
dfsbcq |
|- ( w = q -> ( [. w / p ]. ps <-> [. q / p ]. ps ) ) |
7 |
3 4 5 6
|
reu8nf |
|- ( E! p e. ( Pairs ` X ) ps <-> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) |
8 |
|
sprel |
|- ( p e. ( Pairs ` X ) -> E. a e. X E. b e. X p = { a , b } ) |
9 |
1
|
biimpcd |
|- ( ps -> ( p = { a , b } -> ch ) ) |
10 |
9
|
adantr |
|- ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> ( p = { a , b } -> ch ) ) |
11 |
10
|
ad2antlr |
|- ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) -> ( p = { a , b } -> ch ) ) |
12 |
11
|
imp |
|- ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) -> ch ) |
13 |
|
pm3.22 |
|- ( ( ( x e. X /\ y e. X ) /\ X e. V ) -> ( X e. V /\ ( x e. X /\ y e. X ) ) ) |
14 |
13
|
adantr |
|- ( ( ( ( x e. X /\ y e. X ) /\ X e. V ) /\ ps ) -> ( X e. V /\ ( x e. X /\ y e. X ) ) ) |
15 |
|
prelspr |
|- ( ( X e. V /\ ( x e. X /\ y e. X ) ) -> { x , y } e. ( Pairs ` X ) ) |
16 |
|
dfsbcq |
|- ( q = { x , y } -> ( [. q / p ]. ps <-> [. { x , y } / p ]. ps ) ) |
17 |
|
eqeq2 |
|- ( q = { x , y } -> ( p = q <-> p = { x , y } ) ) |
18 |
16 17
|
imbi12d |
|- ( q = { x , y } -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. { x , y } / p ]. ps -> p = { x , y } ) ) ) |
19 |
18
|
adantl |
|- ( ( ( X e. V /\ ( x e. X /\ y e. X ) ) /\ q = { x , y } ) -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. { x , y } / p ]. ps -> p = { x , y } ) ) ) |
20 |
15 19
|
rspcdv |
|- ( ( X e. V /\ ( x e. X /\ y e. X ) ) -> ( A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) -> ( [. { x , y } / p ]. ps -> p = { x , y } ) ) ) |
21 |
14 20
|
syl |
|- ( ( ( ( x e. X /\ y e. X ) /\ X e. V ) /\ ps ) -> ( A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) -> ( [. { x , y } / p ]. ps -> p = { x , y } ) ) ) |
22 |
|
zfpair2 |
|- { x , y } e. _V |
23 |
22 2
|
sbcie |
|- ( [. { x , y } / p ]. ps <-> th ) |
24 |
|
pm2.27 |
|- ( [. { x , y } / p ]. ps -> ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> p = { x , y } ) ) |
25 |
23 24
|
sylbir |
|- ( th -> ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> p = { x , y } ) ) |
26 |
|
eqcom |
|- ( { x , y } = p <-> p = { x , y } ) |
27 |
25 26
|
syl6ibr |
|- ( th -> ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> { x , y } = p ) ) |
28 |
27
|
com12 |
|- ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> ( th -> { x , y } = p ) ) |
29 |
|
eqeq2 |
|- ( { a , b } = p -> ( { x , y } = { a , b } <-> { x , y } = p ) ) |
30 |
29
|
eqcoms |
|- ( p = { a , b } -> ( { x , y } = { a , b } <-> { x , y } = p ) ) |
31 |
30
|
imbi2d |
|- ( p = { a , b } -> ( ( th -> { x , y } = { a , b } ) <-> ( th -> { x , y } = p ) ) ) |
32 |
28 31
|
syl5ibrcom |
|- ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) ) |
33 |
32
|
a1d |
|- ( ( [. { x , y } / p ]. ps -> p = { x , y } ) -> ( ( a e. X /\ b e. X ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) ) ) |
34 |
21 33
|
syl6 |
|- ( ( ( ( x e. X /\ y e. X ) /\ X e. V ) /\ ps ) -> ( A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) -> ( ( a e. X /\ b e. X ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) ) ) ) |
35 |
34
|
expimpd |
|- ( ( ( x e. X /\ y e. X ) /\ X e. V ) -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> ( ( a e. X /\ b e. X ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) ) ) ) |
36 |
35
|
expimpd |
|- ( ( x e. X /\ y e. X ) -> ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) -> ( ( a e. X /\ b e. X ) -> ( p = { a , b } -> ( th -> { x , y } = { a , b } ) ) ) ) ) |
37 |
36
|
imp4c |
|- ( ( x e. X /\ y e. X ) -> ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) -> ( th -> { x , y } = { a , b } ) ) ) |
38 |
37
|
impcom |
|- ( ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) /\ ( x e. X /\ y e. X ) ) -> ( th -> { x , y } = { a , b } ) ) |
39 |
38
|
ralrimivva |
|- ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) -> A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) |
40 |
12 39
|
jca |
|- ( ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) /\ p = { a , b } ) -> ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) |
41 |
40
|
ex |
|- ( ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) /\ ( a e. X /\ b e. X ) ) -> ( p = { a , b } -> ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) |
42 |
41
|
reximdvva |
|- ( ( X e. V /\ ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) -> ( E. a e. X E. b e. X p = { a , b } -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) |
43 |
42
|
expcom |
|- ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> ( X e. V -> ( E. a e. X E. b e. X p = { a , b } -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) ) |
44 |
43
|
com13 |
|- ( E. a e. X E. b e. X p = { a , b } -> ( X e. V -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) ) |
45 |
8 44
|
syl |
|- ( p e. ( Pairs ` X ) -> ( X e. V -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) ) |
46 |
45
|
impcom |
|- ( ( X e. V /\ p e. ( Pairs ` X ) ) -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) |
47 |
46
|
rexlimdva |
|- ( X e. V -> ( E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) -> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) |
48 |
|
prelspr |
|- ( ( X e. V /\ ( a e. X /\ b e. X ) ) -> { a , b } e. ( Pairs ` X ) ) |
49 |
48
|
adantr |
|- ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> { a , b } e. ( Pairs ` X ) ) |
50 |
|
simprl |
|- ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> ch ) |
51 |
|
nfsbc1v |
|- F/ x [. c / x ]. th |
52 |
|
nfv |
|- F/ x { c , y } = { a , b } |
53 |
51 52
|
nfim |
|- F/ x ( [. c / x ]. th -> { c , y } = { a , b } ) |
54 |
|
nfsbc1v |
|- F/ y [. d / y ]. [. c / x ]. th |
55 |
|
nfv |
|- F/ y { c , d } = { a , b } |
56 |
54 55
|
nfim |
|- F/ y ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) |
57 |
|
sbceq1a |
|- ( x = c -> ( th <-> [. c / x ]. th ) ) |
58 |
|
preq1 |
|- ( x = c -> { x , y } = { c , y } ) |
59 |
58
|
eqeq1d |
|- ( x = c -> ( { x , y } = { a , b } <-> { c , y } = { a , b } ) ) |
60 |
57 59
|
imbi12d |
|- ( x = c -> ( ( th -> { x , y } = { a , b } ) <-> ( [. c / x ]. th -> { c , y } = { a , b } ) ) ) |
61 |
|
sbceq1a |
|- ( y = d -> ( [. c / x ]. th <-> [. d / y ]. [. c / x ]. th ) ) |
62 |
|
preq2 |
|- ( y = d -> { c , y } = { c , d } ) |
63 |
62
|
eqeq1d |
|- ( y = d -> ( { c , y } = { a , b } <-> { c , d } = { a , b } ) ) |
64 |
61 63
|
imbi12d |
|- ( y = d -> ( ( [. c / x ]. th -> { c , y } = { a , b } ) <-> ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) ) ) |
65 |
53 56 60 64
|
rspc2 |
|- ( ( c e. X /\ d e. X ) -> ( A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) -> ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) ) ) |
66 |
65
|
ad2antlr |
|- ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( c e. X /\ d e. X ) ) /\ ch ) -> ( A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) -> ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) ) ) |
67 |
2
|
sbcpr |
|- ( [. { c , d } / p ]. ps <-> [. d / y ]. [. c / x ]. th ) |
68 |
|
pm2.27 |
|- ( [. d / y ]. [. c / x ]. th -> ( ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) -> { c , d } = { a , b } ) ) |
69 |
67 68
|
sylbi |
|- ( [. { c , d } / p ]. ps -> ( ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) -> { c , d } = { a , b } ) ) |
70 |
|
eqcom |
|- ( { a , b } = { c , d } <-> { c , d } = { a , b } ) |
71 |
69 70
|
syl6ibr |
|- ( [. { c , d } / p ]. ps -> ( ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) -> { a , b } = { c , d } ) ) |
72 |
71
|
com12 |
|- ( ( [. d / y ]. [. c / x ]. th -> { c , d } = { a , b } ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) |
73 |
66 72
|
syl6 |
|- ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( c e. X /\ d e. X ) ) /\ ch ) -> ( A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) ) |
74 |
73
|
expimpd |
|- ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( c e. X /\ d e. X ) ) -> ( ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) ) |
75 |
74
|
expcom |
|- ( ( c e. X /\ d e. X ) -> ( ( X e. V /\ ( a e. X /\ b e. X ) ) -> ( ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) ) ) |
76 |
75
|
impd |
|- ( ( c e. X /\ d e. X ) -> ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) ) |
77 |
76
|
impcom |
|- ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) /\ ( c e. X /\ d e. X ) ) -> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) |
78 |
|
dfsbcq |
|- ( q = { c , d } -> ( [. q / p ]. ps <-> [. { c , d } / p ]. ps ) ) |
79 |
|
eqeq2 |
|- ( q = { c , d } -> ( { a , b } = q <-> { a , b } = { c , d } ) ) |
80 |
78 79
|
imbi12d |
|- ( q = { c , d } -> ( ( [. q / p ]. ps -> { a , b } = q ) <-> ( [. { c , d } / p ]. ps -> { a , b } = { c , d } ) ) ) |
81 |
77 80
|
syl5ibrcom |
|- ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) /\ ( c e. X /\ d e. X ) ) -> ( q = { c , d } -> ( [. q / p ]. ps -> { a , b } = q ) ) ) |
82 |
81
|
rexlimdvva |
|- ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> ( E. c e. X E. d e. X q = { c , d } -> ( [. q / p ]. ps -> { a , b } = q ) ) ) |
83 |
|
sprel |
|- ( q e. ( Pairs ` X ) -> E. c e. X E. d e. X q = { c , d } ) |
84 |
82 83
|
impel |
|- ( ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) /\ q e. ( Pairs ` X ) ) -> ( [. q / p ]. ps -> { a , b } = q ) ) |
85 |
84
|
ralrimiva |
|- ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) ) |
86 |
|
nfv |
|- F/ p ch |
87 |
|
nfcv |
|- F/_ p ( Pairs ` X ) |
88 |
|
nfv |
|- F/ p { a , b } = q |
89 |
3 88
|
nfim |
|- F/ p ( [. q / p ]. ps -> { a , b } = q ) |
90 |
87 89
|
nfralw |
|- F/ p A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) |
91 |
86 90
|
nfan |
|- F/ p ( ch /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) ) |
92 |
|
eqeq1 |
|- ( p = { a , b } -> ( p = q <-> { a , b } = q ) ) |
93 |
92
|
imbi2d |
|- ( p = { a , b } -> ( ( [. q / p ]. ps -> p = q ) <-> ( [. q / p ]. ps -> { a , b } = q ) ) ) |
94 |
93
|
ralbidv |
|- ( p = { a , b } -> ( A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) <-> A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) ) ) |
95 |
1 94
|
anbi12d |
|- ( p = { a , b } -> ( ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) <-> ( ch /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) ) ) ) |
96 |
91 95
|
rspce |
|- ( ( { a , b } e. ( Pairs ` X ) /\ ( ch /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> { a , b } = q ) ) ) -> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) |
97 |
49 50 85 96
|
syl12anc |
|- ( ( ( X e. V /\ ( a e. X /\ b e. X ) ) /\ ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) -> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) |
98 |
97
|
ex |
|- ( ( X e. V /\ ( a e. X /\ b e. X ) ) -> ( ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) -> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) ) |
99 |
98
|
rexlimdvva |
|- ( X e. V -> ( E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) -> E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) ) ) |
100 |
47 99
|
impbid |
|- ( X e. V -> ( E. p e. ( Pairs ` X ) ( ps /\ A. q e. ( Pairs ` X ) ( [. q / p ]. ps -> p = q ) ) <-> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) |
101 |
7 100
|
syl5bb |
|- ( X e. V -> ( E! p e. ( Pairs ` X ) ps <-> E. a e. X E. b e. X ( ch /\ A. x e. X A. y e. X ( th -> { x , y } = { a , b } ) ) ) ) |