Step |
Hyp |
Ref |
Expression |
1 |
|
xpsnen.1 |
|- A e. _V |
2 |
|
xpsnen.2 |
|- B e. _V |
3 |
|
snex |
|- { B } e. _V |
4 |
1 3
|
xpex |
|- ( A X. { B } ) e. _V |
5 |
|
elxp |
|- ( y e. ( A X. { B } ) <-> E. x E. z ( y = <. x , z >. /\ ( x e. A /\ z e. { B } ) ) ) |
6 |
|
inteq |
|- ( y = <. x , z >. -> |^| y = |^| <. x , z >. ) |
7 |
6
|
inteqd |
|- ( y = <. x , z >. -> |^| |^| y = |^| |^| <. x , z >. ) |
8 |
|
vex |
|- x e. _V |
9 |
|
vex |
|- z e. _V |
10 |
8 9
|
op1stb |
|- |^| |^| <. x , z >. = x |
11 |
7 10
|
eqtrdi |
|- ( y = <. x , z >. -> |^| |^| y = x ) |
12 |
11 8
|
eqeltrdi |
|- ( y = <. x , z >. -> |^| |^| y e. _V ) |
13 |
12
|
adantr |
|- ( ( y = <. x , z >. /\ ( x e. A /\ z e. { B } ) ) -> |^| |^| y e. _V ) |
14 |
13
|
exlimivv |
|- ( E. x E. z ( y = <. x , z >. /\ ( x e. A /\ z e. { B } ) ) -> |^| |^| y e. _V ) |
15 |
5 14
|
sylbi |
|- ( y e. ( A X. { B } ) -> |^| |^| y e. _V ) |
16 |
|
opex |
|- <. x , B >. e. _V |
17 |
16
|
a1i |
|- ( x e. A -> <. x , B >. e. _V ) |
18 |
|
eqvisset |
|- ( x = |^| |^| y -> |^| |^| y e. _V ) |
19 |
|
ancom |
|- ( ( ( y = <. x , z >. /\ x e. A ) /\ z e. { B } ) <-> ( z e. { B } /\ ( y = <. x , z >. /\ x e. A ) ) ) |
20 |
|
anass |
|- ( ( ( y = <. x , z >. /\ x e. A ) /\ z e. { B } ) <-> ( y = <. x , z >. /\ ( x e. A /\ z e. { B } ) ) ) |
21 |
|
velsn |
|- ( z e. { B } <-> z = B ) |
22 |
21
|
anbi1i |
|- ( ( z e. { B } /\ ( y = <. x , z >. /\ x e. A ) ) <-> ( z = B /\ ( y = <. x , z >. /\ x e. A ) ) ) |
23 |
19 20 22
|
3bitr3i |
|- ( ( y = <. x , z >. /\ ( x e. A /\ z e. { B } ) ) <-> ( z = B /\ ( y = <. x , z >. /\ x e. A ) ) ) |
24 |
23
|
exbii |
|- ( E. z ( y = <. x , z >. /\ ( x e. A /\ z e. { B } ) ) <-> E. z ( z = B /\ ( y = <. x , z >. /\ x e. A ) ) ) |
25 |
|
opeq2 |
|- ( z = B -> <. x , z >. = <. x , B >. ) |
26 |
25
|
eqeq2d |
|- ( z = B -> ( y = <. x , z >. <-> y = <. x , B >. ) ) |
27 |
26
|
anbi1d |
|- ( z = B -> ( ( y = <. x , z >. /\ x e. A ) <-> ( y = <. x , B >. /\ x e. A ) ) ) |
28 |
2 27
|
ceqsexv |
|- ( E. z ( z = B /\ ( y = <. x , z >. /\ x e. A ) ) <-> ( y = <. x , B >. /\ x e. A ) ) |
29 |
|
inteq |
|- ( y = <. x , B >. -> |^| y = |^| <. x , B >. ) |
30 |
29
|
inteqd |
|- ( y = <. x , B >. -> |^| |^| y = |^| |^| <. x , B >. ) |
31 |
8 2
|
op1stb |
|- |^| |^| <. x , B >. = x |
32 |
30 31
|
eqtr2di |
|- ( y = <. x , B >. -> x = |^| |^| y ) |
33 |
32
|
pm4.71ri |
|- ( y = <. x , B >. <-> ( x = |^| |^| y /\ y = <. x , B >. ) ) |
34 |
33
|
anbi1i |
|- ( ( y = <. x , B >. /\ x e. A ) <-> ( ( x = |^| |^| y /\ y = <. x , B >. ) /\ x e. A ) ) |
35 |
|
anass |
|- ( ( ( x = |^| |^| y /\ y = <. x , B >. ) /\ x e. A ) <-> ( x = |^| |^| y /\ ( y = <. x , B >. /\ x e. A ) ) ) |
36 |
34 35
|
bitri |
|- ( ( y = <. x , B >. /\ x e. A ) <-> ( x = |^| |^| y /\ ( y = <. x , B >. /\ x e. A ) ) ) |
37 |
24 28 36
|
3bitri |
|- ( E. z ( y = <. x , z >. /\ ( x e. A /\ z e. { B } ) ) <-> ( x = |^| |^| y /\ ( y = <. x , B >. /\ x e. A ) ) ) |
38 |
37
|
exbii |
|- ( E. x E. z ( y = <. x , z >. /\ ( x e. A /\ z e. { B } ) ) <-> E. x ( x = |^| |^| y /\ ( y = <. x , B >. /\ x e. A ) ) ) |
39 |
5 38
|
bitri |
|- ( y e. ( A X. { B } ) <-> E. x ( x = |^| |^| y /\ ( y = <. x , B >. /\ x e. A ) ) ) |
40 |
|
opeq1 |
|- ( x = |^| |^| y -> <. x , B >. = <. |^| |^| y , B >. ) |
41 |
40
|
eqeq2d |
|- ( x = |^| |^| y -> ( y = <. x , B >. <-> y = <. |^| |^| y , B >. ) ) |
42 |
|
eleq1 |
|- ( x = |^| |^| y -> ( x e. A <-> |^| |^| y e. A ) ) |
43 |
41 42
|
anbi12d |
|- ( x = |^| |^| y -> ( ( y = <. x , B >. /\ x e. A ) <-> ( y = <. |^| |^| y , B >. /\ |^| |^| y e. A ) ) ) |
44 |
43
|
ceqsexgv |
|- ( |^| |^| y e. _V -> ( E. x ( x = |^| |^| y /\ ( y = <. x , B >. /\ x e. A ) ) <-> ( y = <. |^| |^| y , B >. /\ |^| |^| y e. A ) ) ) |
45 |
39 44
|
syl5bb |
|- ( |^| |^| y e. _V -> ( y e. ( A X. { B } ) <-> ( y = <. |^| |^| y , B >. /\ |^| |^| y e. A ) ) ) |
46 |
18 45
|
syl |
|- ( x = |^| |^| y -> ( y e. ( A X. { B } ) <-> ( y = <. |^| |^| y , B >. /\ |^| |^| y e. A ) ) ) |
47 |
46
|
pm5.32ri |
|- ( ( y e. ( A X. { B } ) /\ x = |^| |^| y ) <-> ( ( y = <. |^| |^| y , B >. /\ |^| |^| y e. A ) /\ x = |^| |^| y ) ) |
48 |
32
|
adantr |
|- ( ( y = <. x , B >. /\ x e. A ) -> x = |^| |^| y ) |
49 |
48
|
pm4.71i |
|- ( ( y = <. x , B >. /\ x e. A ) <-> ( ( y = <. x , B >. /\ x e. A ) /\ x = |^| |^| y ) ) |
50 |
43
|
pm5.32ri |
|- ( ( ( y = <. x , B >. /\ x e. A ) /\ x = |^| |^| y ) <-> ( ( y = <. |^| |^| y , B >. /\ |^| |^| y e. A ) /\ x = |^| |^| y ) ) |
51 |
49 50
|
bitr2i |
|- ( ( ( y = <. |^| |^| y , B >. /\ |^| |^| y e. A ) /\ x = |^| |^| y ) <-> ( y = <. x , B >. /\ x e. A ) ) |
52 |
|
ancom |
|- ( ( y = <. x , B >. /\ x e. A ) <-> ( x e. A /\ y = <. x , B >. ) ) |
53 |
47 51 52
|
3bitri |
|- ( ( y e. ( A X. { B } ) /\ x = |^| |^| y ) <-> ( x e. A /\ y = <. x , B >. ) ) |
54 |
4 1 15 17 53
|
en2i |
|- ( A X. { B } ) ~~ A |