Theorem phplem4 4658

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		entr 4555	. . . . . 6 |- ((A ~~ (suc B \ {(f` A)}) /\ (suc B \ {(f` A)}) ~~ B) -> A ~~ B)
2		f1of1 3796	. . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> f:suc A-1-1->suc B)
3		sssucid 3050	. . . . . . . . . 10 |- A (_ suc A
4	2, 3	jctir 291	. . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (f:suc A-1-1->suc B /\ A (_ suc A))
5		f1ores 3811	. . . . . . . . 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 4539	. . . . . . . . 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 3227	. . . . . . . . 9 |- (A e. om -> Ord A)
11		orddif 3065	. . . . . . . . 9 |- (Ord A -> A = (suc A \ {A}))
12		imaeq2 3492	. . . . . . . . 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 3798	. . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> f Fn suc A)
15	6	sucid 3051	. . . . . . . . . . 11 |- A e. suc A
16		fnsnfv 3878	. . . . . . . . . . 11 |- ((f Fn suc A /\ A e. suc A) -> {(f` A)} = (f"{A}))
17	15, 16	mpan2 700	. . . . . . . . . 10 |- (f Fn suc A -> {(f` A)} = (f"{A}))
18		difeq2 2206	. . . . . . . . . 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 3506	. . . . . . . . . . . . 13 |- (f"dom f) = ran f
21	20	eqcomi 1522	. . . . . . . . . . . 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 3803	. . . . . . . . . . . 12 |- (f:suc A-1-1-onto->suc B -> f:suc A-onto->suc B)
24		forn 3782	. . . . . . . . . . . 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 3693	. . . . . . . . . . . 12 |- (f Fn suc A -> dom f = suc A)
27		imaeq2 3492	. . . . . . . . . . . 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 1558	. . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> suc B = (f"suc A))
30	29	difeq1d 2210	. . . . . . . . 9 |- (f:suc A-1-1-onto->suc B -> (suc B \ {(f` A)}) = ((f"suc A) \ {(f` A)}))
31		dff1o3 3802	. . . . . . . . . . 11 |- (f:suc A-1-1-onto->suc B <-> (f:suc A-onto->suc B /\ Fun `'f))
32	31	pm3.27bi 324	. . . . . . . . . 10 |- (f:suc A-1-1-onto->suc B -> Fun `'f)
33		imadif 3679	. . . . . . . . . 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 1561	. . . . . . . 8 |- (f:suc A-1-1-onto->suc B -> (f"(suc A \ {A})) = (suc B \ {(f` A)}))
36	13, 35	sylan9eq 1570	. . . . . . 7 |- ((A e. om /\ f:suc A-1-1-onto->suc B) -> (f"A) = (suc B \ {(f` A)}))
37	9, 36	breqtrd 2712	. . . . . 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 3843	. . . . . . . . 9 |- (f` A) e. V
40	38, 39	phplem3 4657	. . . . . . . 8 |- ((B e. om /\ (f` A) e. suc B) -> B ~~ (suc B \ {(f` A)}))
41		fnfvelrn 3927	. . . . . . . . . . 11 |- ((f Fn suc A /\ A e. suc A) -> (f` A) e. ran f)
42	15, 41	mpan2 700	. . . . . . . . . 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 1584	. . . . . . . . . 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 193	. . . . . . . 8 |- (f:suc A-1-1-onto->suc B -> (f` A) e. suc B)
47	40, 46	sylan2 453	. . . . . . 7 |- ((B e. om /\ f:suc A-1-1-onto->suc B) -> B ~~ (suc B \ {(f` A)}))
48	38	sucex 3168	. . . . . . . . 9 |- suc B e. V
49		difss 2219	. . . . . . . . 9 |- (suc B \ {(f` A)}) (_ suc B
50	48, 49	ssexi 2794	. . . . . . . 8 |- (suc B \ {(f` A)}) e. V
51	50	ensym 4553	. . . . . . 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 456	. . . . 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 516	. . . 4 |- (((A e. om /\ B e. om) /\ f:suc A-1-1-onto->suc B) -> A ~~ B)
55	54	ex 371	. . 3 |- ((A e. om /\ B e. om) -> (f:suc A-1-1-onto->suc B -> A ~~ B))
56	55	19.23adv 1251	. 2 |- ((A e. om /\ B e. om) -> (E.f f:suc A-1-1-onto->suc B -> A ~~ B))
57	48	bren 4518	. 2 |- (suc A ~~ suc B <-> E.f f:suc A-1-1-onto->suc B)
58	56, 57	syl5ib 204	1 |- ((A e. om /\ B e. om) -> (suc A ~~ suc B -> A ~~ B))

Syntax hints:   -> wi 3   <-> wb 144   /\ wa 221   = wceq 992   e. wcel 994  E.wex 1016  Vcvv 1857   \ cdif 2096   (_ wss 2099  {csn 2467   class class class wbr 2692  Ord word 2974  suc csuc 2977  omcom 3218  `'ccnv 3250  dom cdm 3251  ran crn 3252   |` cres 3253  "cima 3254  Fun wfun 3257   Fn wfn 3258  -1-1->wf1 3260  -onto->wfo 3261  -1-1-onto->wf1o 3262  ` cfv 3263   ~~ cen 4505

This theorem is referenced by:  nneneq 4659

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-9 1001  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-rep 2767  ax-sep 2777  ax-nul 2784  ax-pow 2818  ax-pr 2855  ax-un 3089

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-3an 783  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-ral 1695  df-rex 1696  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474  df-uni 2570  df-br 2693  df-opab 2741  df-tr 2755  df-eprel 2910  df-id 2913  df-po 2918  df-so 2929  df-fr 2947  df-we 2962  df-ord 2978  df-on 2979  df-suc 2981  df-om 3219  df-xp 3265  df-rel 3266  df-cnv 3267  df-co 3268  df-dm 3269  df-rn 3270  df-res 3271  df-ima 3272  df-fun 3273  df-fn 3274  df-f 3275  df-f1 3276  df-fo 3277  df-f1o 3278  df-fv 3279  df-er 4401  df-en 4509

Copyright terms: Public domain