ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  xpsnen Structured version   GIF version

Theorem xpsnen 6231
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.)
Hypotheses
Ref Expression
xpsnen.1 A V
xpsnen.2 B V
Assertion
Ref Expression
xpsnen (A × {B}) ≈ A

Proof of Theorem xpsnen
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 xpsnen.1 . . 3 A V
2 xpsnen.2 . . . 4 B V
32snex 3928 . . 3 {B} V
41, 3xpex 4396 . 2 (A × {B}) V
5 elxp 4305 . . 3 (y (A × {B}) ↔ xz(y = ⟨x, z (x A z {B})))
6 inteq 3609 . . . . . . . 8 (y = ⟨x, z⟩ → y = x, z⟩)
76inteqd 3611 . . . . . . 7 (y = ⟨x, z⟩ → y = x, z⟩)
8 vex 2554 . . . . . . . 8 x V
9 vex 2554 . . . . . . . 8 z V
108, 9op1stb 4175 . . . . . . 7 x, z⟩ = x
117, 10syl6eq 2085 . . . . . 6 (y = ⟨x, z⟩ → y = x)
1211, 8syl6eqel 2125 . . . . 5 (y = ⟨x, z⟩ → y V)
1312adantr 261 . . . 4 ((y = ⟨x, z (x A z {B})) → y V)
1413exlimivv 1773 . . 3 (xz(y = ⟨x, z (x A z {B})) → y V)
155, 14sylbi 114 . 2 (y (A × {B}) → y V)
168, 2opex 3957 . . 3 x, B V
1716a1i 9 . 2 (x A → ⟨x, B V)
18 eqvisset 2559 . . . . 5 (x = y y V)
19 ancom 253 . . . . . . . . . . 11 (((y = ⟨x, z x A) z {B}) ↔ (z {B} (y = ⟨x, z x A)))
20 anass 381 . . . . . . . . . . 11 (((y = ⟨x, z x A) z {B}) ↔ (y = ⟨x, z (x A z {B})))
21 elsn 3382 . . . . . . . . . . . 12 (z {B} ↔ z = B)
2221anbi1i 431 . . . . . . . . . . 11 ((z {B} (y = ⟨x, z x A)) ↔ (z = B (y = ⟨x, z x A)))
2319, 20, 223bitr3i 199 . . . . . . . . . 10 ((y = ⟨x, z (x A z {B})) ↔ (z = B (y = ⟨x, z x A)))
2423exbii 1493 . . . . . . . . 9 (z(y = ⟨x, z (x A z {B})) ↔ z(z = B (y = ⟨x, z x A)))
25 opeq2 3541 . . . . . . . . . . . 12 (z = B → ⟨x, z⟩ = ⟨x, B⟩)
2625eqeq2d 2048 . . . . . . . . . . 11 (z = B → (y = ⟨x, z⟩ ↔ y = ⟨x, B⟩))
2726anbi1d 438 . . . . . . . . . 10 (z = B → ((y = ⟨x, z x A) ↔ (y = ⟨x, B x A)))
282, 27ceqsexv 2587 . . . . . . . . 9 (z(z = B (y = ⟨x, z x A)) ↔ (y = ⟨x, B x A))
29 inteq 3609 . . . . . . . . . . . . . 14 (y = ⟨x, B⟩ → y = x, B⟩)
3029inteqd 3611 . . . . . . . . . . . . 13 (y = ⟨x, B⟩ → y = x, B⟩)
318, 2op1stb 4175 . . . . . . . . . . . . 13 x, B⟩ = x
3230, 31syl6req 2086 . . . . . . . . . . . 12 (y = ⟨x, B⟩ → x = y)
3332pm4.71ri 372 . . . . . . . . . . 11 (y = ⟨x, B⟩ ↔ (x = y y = ⟨x, B⟩))
3433anbi1i 431 . . . . . . . . . 10 ((y = ⟨x, B x A) ↔ ((x = y y = ⟨x, B⟩) x A))
35 anass 381 . . . . . . . . . 10 (((x = y y = ⟨x, B⟩) x A) ↔ (x = y (y = ⟨x, B x A)))
3634, 35bitri 173 . . . . . . . . 9 ((y = ⟨x, B x A) ↔ (x = y (y = ⟨x, B x A)))
3724, 28, 363bitri 195 . . . . . . . 8 (z(y = ⟨x, z (x A z {B})) ↔ (x = y (y = ⟨x, B x A)))
3837exbii 1493 . . . . . . 7 (xz(y = ⟨x, z (x A z {B})) ↔ x(x = y (y = ⟨x, B x A)))
395, 38bitri 173 . . . . . 6 (y (A × {B}) ↔ x(x = y (y = ⟨x, B x A)))
40 opeq1 3540 . . . . . . . . 9 (x = y → ⟨x, B⟩ = ⟨ y, B⟩)
4140eqeq2d 2048 . . . . . . . 8 (x = y → (y = ⟨x, B⟩ ↔ y = ⟨ y, B⟩))
42 eleq1 2097 . . . . . . . 8 (x = y → (x A y A))
4341, 42anbi12d 442 . . . . . . 7 (x = y → ((y = ⟨x, B x A) ↔ (y = ⟨ y, B y A)))
4443ceqsexgv 2667 . . . . . 6 ( y V → (x(x = y (y = ⟨x, B x A)) ↔ (y = ⟨ y, B y A)))
4539, 44syl5bb 181 . . . . 5 ( y V → (y (A × {B}) ↔ (y = ⟨ y, B y A)))
4618, 45syl 14 . . . 4 (x = y → (y (A × {B}) ↔ (y = ⟨ y, B y A)))
4746pm5.32ri 428 . . 3 ((y (A × {B}) x = y) ↔ ((y = ⟨ y, B y A) x = y))
4832adantr 261 . . . . 5 ((y = ⟨x, B x A) → x = y)
4948pm4.71i 371 . . . 4 ((y = ⟨x, B x A) ↔ ((y = ⟨x, B x A) x = y))
5043pm5.32ri 428 . . . 4 (((y = ⟨x, B x A) x = y) ↔ ((y = ⟨ y, B y A) x = y))
5149, 50bitr2i 174 . . 3 (((y = ⟨ y, B y A) x = y) ↔ (y = ⟨x, B x A))
52 ancom 253 . . 3 ((y = ⟨x, B x A) ↔ (x A y = ⟨x, B⟩))
5347, 51, 523bitri 195 . 2 ((y (A × {B}) x = y) ↔ (x A y = ⟨x, B⟩))
544, 1, 15, 17, 53en2i 6186 1 (A × {B}) ≈ A
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98   = wceq 1242  wex 1378   wcel 1390  Vcvv 2551  {csn 3367  cop 3370   cint 3606   class class class wbr 3755   × cxp 4286  cen 6155
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935  ax-un 4136
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-uni 3572  df-int 3607  df-br 3756  df-opab 3810  df-mpt 3811  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852  df-en 6158
This theorem is referenced by:  xpsneng  6232  endisj  6234
  Copyright terms: Public domain W3C validator