Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem alephfp 4880

Description: The aleph function has a fixed point. Similar to Proposition 11.18 of [TakeutiZaring] p. 104, except that we construct an actual example of a fixed point rather than just showing its existence. See alephfp2 4881 for an abbreviated version just showing existence.

Hypothesis

Ref	Expression
alephfplem.1

Assertion

Ref	Expression
alephfp

Distinct variable group:   ,

---

Proof of Theorem alephfp

Step	Hyp	Ref	Expression
1		alephfplem.1	. . . 4
2	1	alephfplem4 4879	. . 3
3		isinfcard 4867	. . . 4
4		cardalephex 4866	. . . . 5
5	4	biimpa 416	. . . 4
6	3, 5	sylbir 201	. . 3
7	2, 6	ax-mp 7	. 2
8		alephle 4864	. . . . . . . . 9
9		elirr 4579	. . . . . . . . . 10
10		frfnom 3942	. . . . . . . . . . . . . . 15
11		fneq1 3574	. . . . . . . . . . . . . . . 16
12	1, 11	ax-mp 7	. . . . . . . . . . . . . . 15
13	10, 12	mpbir 190	. . . . . . . . . . . . . 14
14		fnfun 3577	. . . . . . . . . . . . . 14
15	13, 14	ax-mp 7	. . . . . . . . . . . . 13
16		eluniima 3858	. . . . . . . . . . . . 13
17	15, 16	ax-mp 7	. . . . . . . . . . . 12
18	1	alephfplem3 4878	. . . . . . . . . . . . . . 15
19		alephsson 4874	. . . . . . . . . . . . . . . 16
20	19	sseli 2061	. . . . . . . . . . . . . . 15
21		alephord2i 4857	. . . . . . . . . . . . . . 15
22	18, 20, 21	3syl 20	. . . . . . . . . . . . . 14
23	1	alephfplem2 4877	. . . . . . . . . . . . . . . . 17
24		peano2 3145	. . . . . . . . . . . . . . . . . 18
25		fnfvelrn 3804	. . . . . . . . . . . . . . . . . . . 20
26	13, 25	mpan 694	. . . . . . . . . . . . . . . . . . 19
27		fnima 3596	. . . . . . . . . . . . . . . . . . . 20
28	13, 27	ax-mp 7	. . . . . . . . . . . . . . . . . . 19
29	26, 28	syl6eleqr 1556	. . . . . . . . . . . . . . . . . 18
30	24, 29	syl 10	. . . . . . . . . . . . . . . . 17
31	23, 30	eqeltrrd 1546	. . . . . . . . . . . . . . . 16
32		elssuni 2521	. . . . . . . . . . . . . . . 16
33	31, 32	syl 10	. . . . . . . . . . . . . . 15
34	33	sseld 2063	. . . . . . . . . . . . . 14
35	22, 34	syld 27	. . . . . . . . . . . . 13
36	35	r19.23aiv 1740	. . . . . . . . . . . 12
37	17, 36	sylbi 199	. . . . . . . . . . 11
38		eleq2 1532	. . . . . . . . . . . 12
39		eleq2 1532	. . . . . . . . . . . 12
40	38, 39	imbi12d 625	. . . . . . . . . . 11
41	37, 40	mpbii 193	. . . . . . . . . 10
42	9, 41	mtoi 107	. . . . . . . . 9
43	8, 42	anim12i 333	. . . . . . . 8
44		eloni 2953	. . . . . . . . . 10
45		alephon 4845	. . . . . . . . . . . 12
46	45	onord 3090	. . . . . . . . . . 11
47		ordtri4 2979	. . . . . . . . . . 11
48	46, 47	mpan2 695	. . . . . . . . . 10
49	44, 48	syl 10	. . . . . . . . 9
50	49	adantr 389	. . . . . . . 8
51	43, 50	mpbird 196	. . . . . . 7
52		eqeq2 1481	. . . . . . . 8
53	52	adantl 388	. . . . . . 7
54	51, 53	mpbird 196	. . . . . 6
55	54	eqcomd 1477	. . . . 5
56	55	fveq2d 3719	. . . 4
57		eqeq2 1481	. . . . 5
58	57	adantl 388	. . . 4
59	56, 58	mpbird 196	. . 3
60	59	r19.23aiva 1741	. 2
61	7, 60	ax-mp 7	1

Colors of variables: wff set class

Syntax hints:   wn 2   wi 3   wb 146   wa 223   wceq 954   wcel 956  wrex 1643   wss 2043  c0 2276  cuni 2498  copab 2661   word 2942  con0 2943   csuc 2945  com 3126   crn 3166   cres 3167  cima 3168   wfun 3171   wfn 3172  cfv 3177  crdg 3922  ccrd 4793  cale 4794

This theorem is referenced by:  alephfp2 4881

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-9 963  ax-10 964  ax-11 965  ax-12 966  ax-13 967  ax-14 968  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457  ax-rep 2688  ax-sep 2698  ax-nul 2705  ax-pow 2737  ax-pr 2774  ax-un 2861  ax-reg 4573  ax-inf2 4605  ax-ac 4724

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3or 775  df-3an 776  df-ex 979  df-sb 1170  df-eu 1380  df-mo 1381  df-clab 1462  df-cleq 1467  df-clel 1470  df-ne 1584  df-ral 1646  df-rex 1647  df-reu 1648  df-rab 1649  df-v 1808  df-sbc 1938  df-dif 2045  df-un 2046  df-in 2047  df-ss 2049  df-pss 2051  df-nul 2277  df-if 2358  df-pw 2398  df-sn 2408  df-pr 2409  df-tp 2411  df-op 2412  df-uni 2499  df-int 2529