Metamath Proof Explorer


Theorem xpsnen

Description: A set is equinumerous to its Cartesian product with a singleton. Proposition 4.22(c) of Mendelson p. 254. (Contributed by NM, 4-Jan-2004) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Hypotheses xpsnen.1
|- A e. _V
xpsnen.2
|- B e. _V
Assertion xpsnen
|- ( A X. { B } ) ~~ A

Proof

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