Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  sucxpdom Structured version   Unicode version

Theorem sucxpdom 7783
 Description: Cartesian product dominates successor for set with cardinality greater than 1. Proposition 10.38 of [TakeutiZaring] p. 93 (but generalized to arbitrary sets, not just ordinals). (Contributed by NM, 3-Sep-2004.) (Proof shortened by Mario Carneiro, 27-Apr-2015.)
Assertion
Ref Expression
sucxpdom

Proof of Theorem sucxpdom
StepHypRef Expression
1 df-suc 5444 . 2
2 relsdom 7580 . . . . . . . . 9
32brrelex2i 4891 . . . . . . . 8
4 1on 7193 . . . . . . . 8
5 xpsneng 7659 . . . . . . . 8
63, 4, 5sylancl 666 . . . . . . 7
76ensymd 7623 . . . . . 6
8 endom 7599 . . . . . 6
97, 8syl 17 . . . . 5
10 ensn1g 7637 . . . . . . . . 9
113, 10syl 17 . . . . . . . 8
12 ensdomtr 7710 . . . . . . . 8
1311, 12mpancom 673 . . . . . . 7
14 0ex 4552 . . . . . . . . 9
15 xpsneng 7659 . . . . . . . . 9
163, 14, 15sylancl 666 . . . . . . . 8
1716ensymd 7623 . . . . . . 7
18 sdomentr 7708 . . . . . . 7
1913, 17, 18syl2anc 665 . . . . . 6
20 sdomdom 7600 . . . . . 6
2119, 20syl 17 . . . . 5
22 1n0 7201 . . . . . 6
23 xpsndisj 5275 . . . . . 6
2422, 23mp1i 13 . . . . 5
25 undom 7662 . . . . 5
269, 21, 24, 25syl21anc 1263 . . . 4
27 sdomentr 7708 . . . . . 6
287, 27mpdan 672 . . . . 5
29 sdomentr 7708 . . . . . 6
3017, 29mpdan 672 . . . . 5
31 unxpdom 7781 . . . . 5
3228, 30, 31syl2anc 665 . . . 4
33 domtr 7625 . . . 4
3426, 32, 33syl2anc 665 . . 3
35 xpen 7737 . . . 4
366, 16, 35syl2anc 665 . . 3
37 domentr 7631 . . 3
3834, 36, 37syl2anc 665 . 2
391, 38syl5eqbr 4454 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1437   wcel 1868   wne 2618  cvv 3081   cun 3434   cin 3435  c0 3761  csn 3996   class class class wbr 4420   cxp 4847  con0 5438   csuc 5440  c1o 7179   cen 7570   cdom 7571   csdm 7572 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-tp 4001  df-op 4003  df-uni 4217  df-int 4253  df-br 4421  df-opab 4480  df-mpt 4481  df-tr 4516  df-eprel 4760  df-id 4764  df-po 4770  df-so 4771  df-fr 4808  df-we 4810  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-ord 5441  df-on 5442  df-lim 5443  df-suc 5444  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-om 6703  df-1st 6803  df-2nd 6804  df-1o 7186  df-2o 7187  df-er 7367  df-en 7574  df-dom 7575  df-sdom 7576 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator