This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid 
 |-  ( |^| |^| 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