rankcf

Description: Any set must be at least as large as the cofinality of its rank, because the ranks of the elements of A form a cofinal map into ( rankA ) . (Contributed by Mario Carneiro, 27-May-2013)

		Ref	Expression
	Assertion	rankcf	$⊢ \neg A ≺ cf (rank (A))$

Proof

Step	Hyp	Ref	Expression
1		rankon	$⊢ rank (A) \in On$
2		onzsl	$⊢ rank (A) \in On \leftrightarrow (rank (A) = \emptyset \lor \exists x \in On rank (A) = suc x \lor (rank (A) \in V \land Lim rank (A)))$
3	1 2	mpbi	$⊢ (rank (A) = \emptyset \lor \exists x \in On rank (A) = suc x \lor (rank (A) \in V \land Lim rank (A)))$
4		sdom0	$⊢ \neg A ≺ \emptyset$
5		fveq2	$⊢ rank (A) = \emptyset \to cf (rank (A)) = cf (\emptyset)$
6		cf0	$⊢ cf (\emptyset) = \emptyset$
7	5 6	eqtrdi	$⊢ rank (A) = \emptyset \to cf (rank (A)) = \emptyset$
8	7	breq2d	$⊢ rank (A) = \emptyset \to (A ≺ cf (rank (A)) \leftrightarrow A ≺ \emptyset)$
9	4 8	mtbiri	$⊢ rank (A) = \emptyset \to \neg A ≺ cf (rank (A))$
10		fveq2	$⊢ rank (A) = suc x \to cf (rank (A)) = cf (suc x)$
11		cfsuc	$⊢ x \in On \to cf (suc x) = 1_{𝑜}$
12	10 11	sylan9eqr	$⊢ (x \in On \land rank (A) = suc x) \to cf (rank (A)) = 1_{𝑜}$
13		nsuceq0	$⊢ suc x \neq \emptyset$
14		neeq1	$⊢ rank (A) = suc x \to (rank (A) \neq \emptyset \leftrightarrow suc x \neq \emptyset)$
15	13 14	mpbiri	$⊢ rank (A) = suc x \to rank (A) \neq \emptyset$
16		fveq2	$⊢ A = \emptyset \to rank (A) = rank (\emptyset)$
17		0elon	$⊢ \emptyset \in On$
18		r1fnon	$⊢ R_{1} Fn On$
19	18	fndmi	$⊢ dom R_{1} = On$
20	17 19	eleqtrri	$⊢ \emptyset \in dom R_{1}$
21		rankonid	$⊢ \emptyset \in dom R_{1} \leftrightarrow rank (\emptyset) = \emptyset$
22	20 21	mpbi	$⊢ rank (\emptyset) = \emptyset$
23	16 22	eqtrdi	$⊢ A = \emptyset \to rank (A) = \emptyset$
24	23	necon3i	$⊢ rank (A) \neq \emptyset \to A \neq \emptyset$
25		rankvaln	$⊢ \neg A \in ⋃ R_{1} [On] \to rank (A) = \emptyset$
26	25	necon1ai	$⊢ rank (A) \neq \emptyset \to A \in ⋃ R_{1} [On]$
27		breq2	$⊢ y = A \to (1_{𝑜} ≼ y \leftrightarrow 1_{𝑜} ≼ A)$
28		neeq1	$⊢ y = A \to (y \neq \emptyset \leftrightarrow A \neq \emptyset)$
29		0sdom1dom	$⊢ \emptyset ≺ y \leftrightarrow 1_{𝑜} ≼ y$
30		vex	$⊢ y \in V$
31	30	0sdom	$⊢ \emptyset ≺ y \leftrightarrow y \neq \emptyset$
32	29 31	bitr3i	$⊢ 1_{𝑜} ≼ y \leftrightarrow y \neq \emptyset$
33	27 28 32	vtoclbg	$⊢ A \in ⋃ R_{1} [On] \to (1_{𝑜} ≼ A \leftrightarrow A \neq \emptyset)$
34	26 33	syl	$⊢ rank (A) \neq \emptyset \to (1_{𝑜} ≼ A \leftrightarrow A \neq \emptyset)$
35	24 34	mpbird	$⊢ rank (A) \neq \emptyset \to 1_{𝑜} ≼ A$
36	15 35	syl	$⊢ rank (A) = suc x \to 1_{𝑜} ≼ A$
37	36	adantl	$⊢ (x \in On \land rank (A) = suc x) \to 1_{𝑜} ≼ A$
38	12 37	eqbrtrd	$⊢ (x \in On \land rank (A) = suc x) \to cf (rank (A)) ≼ A$
39	38	rexlimiva	$⊢ \exists x \in On rank (A) = suc x \to cf (rank (A)) ≼ A$
40		domnsym	$⊢ cf (rank (A)) ≼ A \to \neg A ≺ cf (rank (A))$
41	39 40	syl	$⊢ \exists x \in On rank (A) = suc x \to \neg A ≺ cf (rank (A))$
42		nlim0	$⊢ \neg Lim \emptyset$
43		limeq	$⊢ rank (A) = \emptyset \to (Lim rank (A) \leftrightarrow Lim \emptyset)$
44	42 43	mtbiri	$⊢ rank (A) = \emptyset \to \neg Lim rank (A)$
45	25 44	syl	$⊢ \neg A \in ⋃ R_{1} [On] \to \neg Lim rank (A)$
46	45	con4i	$⊢ Lim rank (A) \to A \in ⋃ R_{1} [On]$
47		r1elssi	$⊢ A \in ⋃ R_{1} [On] \to A \subseteq ⋃ R_{1} [On]$
48	46 47	syl	$⊢ Lim rank (A) \to A \subseteq ⋃ R_{1} [On]$
49	48	sselda	$⊢ (Lim rank (A) \land x \in A) \to x \in ⋃ R_{1} [On]$
50		ranksnb	$⊢ x \in ⋃ R_{1} [On] \to rank (\{x\}) = suc rank (x)$
51	49 50	syl	$⊢ (Lim rank (A) \land x \in A) \to rank (\{x\}) = suc rank (x)$
52		rankelb	$⊢ A \in ⋃ R_{1} [On] \to (x \in A \to rank (x) \in rank (A))$
53	46 52	syl	$⊢ Lim rank (A) \to (x \in A \to rank (x) \in rank (A))$
54		limsuc	$⊢ Lim rank (A) \to (rank (x) \in rank (A) \leftrightarrow suc rank (x) \in rank (A))$
55	53 54	sylibd	$⊢ Lim rank (A) \to (x \in A \to suc rank (x) \in rank (A))$
56	55	imp	$⊢ (Lim rank (A) \land x \in A) \to suc rank (x) \in rank (A)$
57	51 56	eqeltrd	$⊢ (Lim rank (A) \land x \in A) \to rank (\{x\}) \in rank (A)$
58		eleq1a	$⊢ rank (\{x\}) \in rank (A) \to (w = rank (\{x\}) \to w \in rank (A))$
59	57 58	syl	$⊢ (Lim rank (A) \land x \in A) \to (w = rank (\{x\}) \to w \in rank (A))$
60	59	rexlimdva	$⊢ Lim rank (A) \to (\exists x \in A w = rank (\{x\}) \to w \in rank (A))$
61	60	abssdv	$⊢ Lim rank (A) \to \{w \| \exists x \in A w = rank (\{x\})\} \subseteq rank (A)$
62		snex	$⊢ \{x\} \in V$
63	62	dfiun2	$⊢ ⋃_{x \in A} \{x\} = ⋃ \{y \| \exists x \in A y = \{x\}\}$
64		iunid	$⊢ ⋃_{x \in A} \{x\} = A$
65	63 64	eqtr3i	$⊢ ⋃ \{y \| \exists x \in A y = \{x\}\} = A$
66	65	fveq2i	$⊢ rank (⋃ \{y \| \exists x \in A y = \{x\}\}) = rank (A)$
67	47	sselda	$⊢ (A \in ⋃ R_{1} [On] \land x \in A) \to x \in ⋃ R_{1} [On]$
68		snwf	$⊢ x \in ⋃ R_{1} [On] \to \{x\} \in ⋃ R_{1} [On]$
69		eleq1a	$⊢ \{x\} \in ⋃ R_{1} [On] \to (y = \{x\} \to y \in ⋃ R_{1} [On])$
70	67 68 69	3syl	$⊢ (A \in ⋃ R_{1} [On] \land x \in A) \to (y = \{x\} \to y \in ⋃ R_{1} [On])$
71	70	rexlimdva	$⊢ A \in ⋃ R_{1} [On] \to (\exists x \in A y = \{x\} \to y \in ⋃ R_{1} [On])$
72	71	abssdv	$⊢ A \in ⋃ R_{1} [On] \to \{y \| \exists x \in A y = \{x\}\} \subseteq ⋃ R_{1} [On]$
73		abrexexg	$⊢ A \in ⋃ R_{1} [On] \to \{y \| \exists x \in A y = \{x\}\} \in V$
74		eleq1	$⊢ z = \{y \| \exists x \in A y = \{x\}\} \to (z \in ⋃ R_{1} [On] \leftrightarrow \{y \| \exists x \in A y = \{x\}\} \in ⋃ R_{1} [On])$
75		sseq1	$⊢ z = \{y \| \exists x \in A y = \{x\}\} \to (z \subseteq ⋃ R_{1} [On] \leftrightarrow \{y \| \exists x \in A y = \{x\}\} \subseteq ⋃ R_{1} [On])$
76		vex	$⊢ z \in V$
77	76	r1elss	$⊢ z \in ⋃ R_{1} [On] \leftrightarrow z \subseteq ⋃ R_{1} [On]$
78	74 75 77	vtoclbg	$⊢ \{y \| \exists x \in A y = \{x\}\} \in V \to (\{y \| \exists x \in A y = \{x\}\} \in ⋃ R_{1} [On] \leftrightarrow \{y \| \exists x \in A y = \{x\}\} \subseteq ⋃ R_{1} [On])$
79	73 78	syl	$⊢ A \in ⋃ R_{1} [On] \to (\{y \| \exists x \in A y = \{x\}\} \in ⋃ R_{1} [On] \leftrightarrow \{y \| \exists x \in A y = \{x\}\} \subseteq ⋃ R_{1} [On])$
80	72 79	mpbird	$⊢ A \in ⋃ R_{1} [On] \to \{y \| \exists x \in A y = \{x\}\} \in ⋃ R_{1} [On]$
81		rankuni2b	$⊢ \{y \| \exists x \in A y = \{x\}\} \in ⋃ R_{1} [On] \to rank (⋃ \{y \| \exists x \in A y = \{x\}\}) = ⋃_{z \in \{y \| \exists x \in A y = \{x\}\}} rank (z)$
82	80 81	syl	$⊢ A \in ⋃ R_{1} [On] \to rank (⋃ \{y \| \exists x \in A y = \{x\}\}) = ⋃_{z \in \{y \| \exists x \in A y = \{x\}\}} rank (z)$
83	66 82	syl5eqr	$⊢ A \in ⋃ R_{1} [On] \to rank (A) = ⋃_{z \in \{y \| \exists x \in A y = \{x\}\}} rank (z)$
84		fvex	$⊢ rank (z) \in V$
85	84	dfiun2	$⊢ ⋃_{z \in \{y \| \exists x \in A y = \{x\}\}} rank (z) = ⋃ \{w \| \exists z \in \{y \| \exists x \in A y = \{x\}\} w = rank (z)\}$
86		fveq2	$⊢ z = \{x\} \to rank (z) = rank (\{x\})$
87	62 86	abrexco	$⊢ \{w \| \exists z \in \{y \| \exists x \in A y = \{x\}\} w = rank (z)\} = \{w \| \exists x \in A w = rank (\{x\})\}$
88	87	unieqi	$⊢ ⋃ \{w \| \exists z \in \{y \| \exists x \in A y = \{x\}\} w = rank (z)\} = ⋃ \{w \| \exists x \in A w = rank (\{x\})\}$
89	85 88	eqtri	$⊢ ⋃_{z \in \{y \| \exists x \in A y = \{x\}\}} rank (z) = ⋃ \{w \| \exists x \in A w = rank (\{x\})\}$
90	83 89	eqtr2di	$⊢ A \in ⋃ R_{1} [On] \to ⋃ \{w \| \exists x \in A w = rank (\{x\})\} = rank (A)$
91	46 90	syl	$⊢ Lim rank (A) \to ⋃ \{w \| \exists x \in A w = rank (\{x\})\} = rank (A)$
92		fvex	$⊢ rank (A) \in V$
93	92	cfslb	$⊢ (Lim rank (A) \land \{w \| \exists x \in A w = rank (\{x\})\} \subseteq rank (A) \land ⋃ \{w \| \exists x \in A w = rank (\{x\})\} = rank (A)) \to cf (rank (A)) ≼ \{w \| \exists x \in A w = rank (\{x\})\}$
94	61 91 93	mpd3an23	$⊢ Lim rank (A) \to cf (rank (A)) ≼ \{w \| \exists x \in A w = rank (\{x\})\}$
95		2fveq3	$⊢ y = A \to cf (rank (y)) = cf (rank (A))$
96		breq12	$⊢ (y = A \land cf (rank (y)) = cf (rank (A))) \to (y ≺ cf (rank (y)) \leftrightarrow A ≺ cf (rank (A)))$
97	95 96	mpdan	$⊢ y = A \to (y ≺ cf (rank (y)) \leftrightarrow A ≺ cf (rank (A)))$
98		rexeq	$⊢ y = A \to (\exists x \in y w = rank (\{x\}) \leftrightarrow \exists x \in A w = rank (\{x\}))$
99	98	abbidv	$⊢ y = A \to \{w \| \exists x \in y w = rank (\{x\})\} = \{w \| \exists x \in A w = rank (\{x\})\}$
100		breq12	$⊢ (\{w \| \exists x \in y w = rank (\{x\})\} = \{w \| \exists x \in A w = rank (\{x\})\} \land y = A) \to (\{w \| \exists x \in y w = rank (\{x\})\} ≼ y \leftrightarrow \{w \| \exists x \in A w = rank (\{x\})\} ≼ A)$
101	99 100	mpancom	$⊢ y = A \to (\{w \| \exists x \in y w = rank (\{x\})\} ≼ y \leftrightarrow \{w \| \exists x \in A w = rank (\{x\})\} ≼ A)$
102	97 101	imbi12d	$⊢ y = A \to ((y ≺ cf (rank (y)) \to \{w \| \exists x \in y w = rank (\{x\})\} ≼ y) \leftrightarrow (A ≺ cf (rank (A)) \to \{w \| \exists x \in A w = rank (\{x\})\} ≼ A))$
103		eqid	$⊢ (x \in y ⟼ rank (\{x\})) = (x \in y ⟼ rank (\{x\}))$
104	103	rnmpt	$⊢ ran (x \in y ⟼ rank (\{x\})) = \{w \| \exists x \in y w = rank (\{x\})\}$
105		cfon	$⊢ cf (rank (y)) \in On$
106		sdomdom	$⊢ y ≺ cf (rank (y)) \to y ≼ cf (rank (y))$
107		ondomen	$⊢ (cf (rank (y)) \in On \land y ≼ cf (rank (y))) \to y \in dom card$
108	105 106 107	sylancr	$⊢ y ≺ cf (rank (y)) \to y \in dom card$
109		fvex	$⊢ rank (\{x\}) \in V$
110	109 103	fnmpti	$⊢ (x \in y ⟼ rank (\{x\})) Fn y$
111		dffn4	$⊢ (x \in y ⟼ rank (\{x\})) Fn y \leftrightarrow (x \in y ⟼ rank (\{x\})) : y \underset{onto}{⟶} ran (x \in y ⟼ rank (\{x\}))$
112	110 111	mpbi	$⊢ (x \in y ⟼ rank (\{x\})) : y \underset{onto}{⟶} ran (x \in y ⟼ rank (\{x\}))$
113		fodomnum	$⊢ y \in dom card \to ((x \in y ⟼ rank (\{x\})) : y \underset{onto}{⟶} ran (x \in y ⟼ rank (\{x\})) \to ran (x \in y ⟼ rank (\{x\})) ≼ y)$
114	108 112 113	mpisyl	$⊢ y ≺ cf (rank (y)) \to ran (x \in y ⟼ rank (\{x\})) ≼ y$
115	104 114	eqbrtrrid	$⊢ y ≺ cf (rank (y)) \to \{w \| \exists x \in y w = rank (\{x\})\} ≼ y$
116	102 115	vtoclg	$⊢ A \in ⋃ R_{1} [On] \to (A ≺ cf (rank (A)) \to \{w \| \exists x \in A w = rank (\{x\})\} ≼ A)$
117	46 116	syl	$⊢ Lim rank (A) \to (A ≺ cf (rank (A)) \to \{w \| \exists x \in A w = rank (\{x\})\} ≼ A)$
118		domtr	$⊢ (cf (rank (A)) ≼ \{w \| \exists x \in A w = rank (\{x\})\} \land \{w \| \exists x \in A w = rank (\{x\})\} ≼ A) \to cf (rank (A)) ≼ A$
119	118 40	syl	$⊢ (cf (rank (A)) ≼ \{w \| \exists x \in A w = rank (\{x\})\} \land \{w \| \exists x \in A w = rank (\{x\})\} ≼ A) \to \neg A ≺ cf (rank (A))$
120	94 117 119	syl6an	$⊢ Lim rank (A) \to (A ≺ cf (rank (A)) \to \neg A ≺ cf (rank (A)))$
121	120	pm2.01d	$⊢ Lim rank (A) \to \neg A ≺ cf (rank (A))$
122	121	adantl	$⊢ (rank (A) \in V \land Lim rank (A)) \to \neg A ≺ cf (rank (A))$
123	9 41 122	3jaoi	$⊢ (rank (A) = \emptyset \lor \exists x \in On rank (A) = suc x \lor (rank (A) \in V \land Lim rank (A))) \to \neg A ≺ cf (rank (A))$
124	3 123	ax-mp	$⊢ \neg A ≺ cf (rank (A))$

Metamath Proof Explorer

Theorem rankcf

Proof