Theorem phplem4 4511

Description: Lemma for Pigeonhole Principle. Equinumerosity of successors implies equinumerosity of the original natural numbers.

Hypotheses

Ref	Expression
phplem2.1	|- A e. V
phplem2.2	|- B e. V

Assertion

Ref	Expression
phplem4	|- ((A e. om /\ B e. om) -> (suc A ~~ suc B -> A ~~ B))

Proof of Theorem phplem4

Step	Hyp	Ref	Expression
1		entrt 4414	. . . . . 6 |- ((A ~~ (suc B \ {(f` A)}) /\ (suc B \ {(f` A)}) ~~ B) -> A ~~ B)
2		f1of1 3688	. . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> f:suc A-1-1->suc B)
3		sssucid 3047	. . . . . . . . . 10 |- A (_ suc A
4	2, 3	jctir 293	. . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (f:suc A-1-1->suc B /\ A (_ suc A))
5		f1ores 3703	. . . . . . . . 9 |- ((f:suc A-1-1->suc B /\ A (_ suc A) -> (f |` A):A-1-1-onto->(f"A))
6		phplem2.1	. . . . . . . . . 10 |- A e. V
7	6	f1oen 4398	. . . . . . . . 9 |- ((f |` A):A-1-1-onto->(f"A) -> A ~~ (f"A))
8	4, 5, 7	3syl 20	. . . . . . . 8 |- (f:suc A-1-1-onto->suc B -> A ~~ (f"A))
9	8	adantl 388	. . . . . . 7 |- ((A e. om /\ f:suc A-1-1-onto->suc B) -> A ~~ (f"A))
10		nnord 3140	. . . . . . . . 9 |- (A e. om -> Ord A)
11		orddif 3075	. . . . . . . . 9 |- (Ord A -> A = (suc A \ {A}))
12		imaeq2 3402	. . . . . . . . 9 |- (A = (suc A \ {A}) -> (f"A) = (f"(suc A \ {A})))
13	10, 11, 12	3syl 20	. . . . . . . 8 |- (A e. om -> (f"A) = (f"(suc A \ {A})))
14		f1ofn 3690	. . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> f Fn suc A)
15	6	sucid 3051	. . . . . . . . . . 11 |- A e. suc A
16		fnsnfv 3767	. . . . . . . . . . 11 |- ((f Fn suc A /\ A e. suc A) -> {(f` A)} = (f"{A}))
17	15, 16	mpan2 696	. . . . . . . . . 10 |- (f Fn suc A -> {(f` A)} = (f"{A}))
18		difeq2 2154	. . . . . . . . . 10 |- ({(f` A)} = (f"{A}) -> ((f"suc A) \ {(f` A)}) = ((f"suc A) \ (f"{A})))
19	14, 17, 18	3syl 20	. . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> ((f"suc A) \ {(f` A)}) = ((f"suc A) \ (f"{A})))
20		imadmrn 3414	. . . . . . . . . . . . 13 |- (f"dom f) = ran f
21	20	eqcomi 1479	. . . . . . . . . . . 12 |- ran f = (f"dom f)
22	21	a1i 8	. . . . . . . . . . 11 |- (f:suc A-1-1-onto->suc B -> ran f = (f"dom f))
23		f1ofo 3695	. . . . . . . . . . . 12 |- (f:suc A-1-1-onto->suc B -> f:suc A-onto->suc B)
24		forn 3674	. . . . . . . . . . . 12 |- (f:suc A-onto->suc B -> ran f = suc B)
25	23, 24	syl 10	. . . . . . . . . . 11 |- (f:suc A-1-1-onto->suc B -> ran f = suc B)
26		fndm 3587	. . . . . . . . . . . 12 |- (f Fn suc A -> dom f = suc A)
27		imaeq2 3402	. . . . . . . . . . . 12 |- (dom f = suc A -> (f"dom f) = (f"suc A))
28	14, 26, 27	3syl 20	. . . . . . . . . . 11 |- (f:suc A-1-1-onto->suc B -> (f"dom f) = (f"suc A))
29	22, 25, 28	3eqtr3d 1515	. . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> suc B = (f"suc A))
30	29	difeq1d 2158	. . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (suc B \ {(f` A)}) = ((f"suc A) \ {(f` A)}))
31		f1o3 3694	. . . . . . . . . . 11 |- (f:suc A-1-1-onto->suc B <-> (f:suc A-onto->suc B /\ Fun `'f))
32	31	pm3.27bi 326	. . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> Fun `'f)
33		imadif 3574	. . . . . . . . . 10 |- (Fun `'f -> (f"(suc A \ {A})) = ((f"suc A) \ (f"{A})))
34	32, 33	syl 10	. . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (f"(suc A \ {A})) = ((f"suc A) \ (f"{A})))
35	19, 30, 34	3eqtr4rd 1518	. . . . . . . 8 |- (f:suc A-1-1-onto->suc B -> (f"(suc A \ {A})) = (suc B \ {(f` A)}))
36	13, 35	sylan9eq 1527	. . . . . . 7 |- ((A e. om /\ f:suc A-1-1-onto->suc B) -> (f"A) = (suc B \ {(f` A)}))
37	9, 36	breqtrd 2639	. . . . . 6 |- ((A e. om /\ f:suc A-1-1-onto->suc B) -> A ~~ (suc B \ {(f` A)}))
38		phplem2.2	. . . . . . . . 9 |- B e. V
39		fvex 3732	. . . . . . . . 9 |- (f` A) e. V
40	38, 39	phplem3 4510	. . . . . . . 8 |- ((B e. om /\ (f` A) e. suc B) -> B ~~ (suc B \ {(f` A)}))
41		fnfvelrn 3813	. . . . . . . . . . 11 |- ((f Fn suc A /\ A e. suc A) -> (f` A) e. ran f)
42	15, 41	mpan2 696	. . . . . . . . . 10 |- (f Fn suc A -> (f` A) e. ran f)
43	14, 42	syl 10	. . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (f` A) e. ran f)
44	24	eleq2d 1541	. . . . . . . . . 10 |- (f:suc A-onto->suc B -> ((f` A) e. ran f <-> (f` A) e. suc B))
45	23, 44	syl 10	. . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> ((f` A) e. ran f <-> (f` A) e. suc B))
46	43, 45	mpbid 195	. . . . . . . 8 |- (f:suc A-1-1-onto->suc B -> (f` A) e. suc B)
47	40, 46	sylan2 451	. . . . . . 7 |- ((B e. om /\ f:suc A-1-1-onto->suc B) -> B ~~ (suc B \ {(f` A)}))
48	38	sucex 3050	. . . . . . . . 9 |- suc B e. V
49		difss 2167	. . . . . . . . 9 |- (suc B \ {(f` A)}) (_ suc B
50	48, 49	ssexi 2720	. . . . . . . 8 |- (suc B \ {(f` A)}) e. V
51	50	ensym 4412	. . . . . . 7 |- (B ~~ (suc B \ {(f` A)}) -> (suc B \ {(f` A)}) ~~ B)
52	47, 51	syl 10	. . . . . 6 |- ((B e. om /\ f:suc A-1-1-onto->suc B) -> (suc B \ {(f` A)}) ~~ B)
53	1, 37, 52	syl2an 454	. . . . 5 |- (((A e. om /\ f:suc A-1-1-onto->suc B) /\ (B e. om /\ f:suc A-1-1-onto->suc B)) -> A ~~ B)
54	53	anandirs 513	. . . 4 |- (((A e. om /\ B e. om) /\ f:suc A-1-1-onto->suc B) -> A ~~ B)
55	54	ex 373	. . 3 |- ((A e. om /\ B e. om) -> (f:suc A-1-1-onto->suc B -> A ~~ B))
56	55	19.23adv 1214	. 2 |- ((A e. om /\ B e. om) -> (E.f f:suc A-1-1-onto->suc B -> A ~~ B))
57	48	bren 4377	. 2 |- (suc A ~~ suc B <-> E.f f:suc A-1-1-onto->suc B)
58	56, 57	syl5ib 206	1 |- ((A e. om /\ B e. om) -> (suc A ~~ suc B -> A ~~ B))

Syntax hints:   -> wi 3   <-> wb 146   /\ wa 223   = wceq 956   e. wcel 958  E.wex 980  Vcvv 1811   \ cdif 2044   (_ wss 2047  {csn 2409   class class class wbr 2619  Ord word 2947  suc csuc 2950  omcom 3131  `'ccnv 3169  dom cdm 3170  ran crn 3171   |` cres 3172  "cima 3173  Fun wfun 3176   Fn wfn 3177  -1-1->wf1 3179  -onto->wfo 3180  -1-1-onto->wf1o 3181  ` cfv 3182   ~~ cen 4364

This theorem is referenced by:  nneneq 4512

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-9 965  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-rep 2693  ax-sep 2703  ax-nul 2710  ax-pow 2742  ax-pr 2779  ax-un 2866

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 777  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-ral 1649  df-rex 1650  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416  df-uni 2504  df-br 2620  df-opab 2667  df-tr 2681  df-eprel 2832  df-id 2835  df-po 2840  df-so 2850  df-fr 2917  df-we 2934  df-ord 2951  df-on 2952  df-suc 2954  df-om 3132  df-xp 3184  df-rel 3185  df-cnv 3186  df-co 3187  df-dm 3188  df-rn 3189  df-res 3190  df-ima 3191  df-fun 3192  df-fn 3193  df-f 3194  df-f1 3195  df-fo 3196  df-f1o 3197  df-fv 3198  df-er 4261  df-en 4368

Copyright terms: Public domain