cff1

Description: There is always a map from ( cfA ) to A (this is a stronger condition than the definition, which only presupposes a map from some y ~( cfA ) . (Contributed by Mario Carneiro, 28-Feb-2013)

		Ref	Expression
	Assertion	cff1	$⊢ A \in On \to \exists f (f : cf (A) \underset{1-1}{⟶} A \land \forall z \in A \exists w \in cf (A) z \subseteq f (w))$

Proof

Step	Hyp	Ref	Expression
1		cfval	$⊢ A \in On \to cf (A) = ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\}$
2		cardon	$⊢ card (y) \in On$
3		eleq1	$⊢ x = card (y) \to (x \in On \leftrightarrow card (y) \in On)$
4	2 3	mpbiri	$⊢ x = card (y) \to x \in On$
5	4	adantr	$⊢ (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to x \in On$
6	5	exlimiv	$⊢ \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to x \in On$
7	6	abssi	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \subseteq On$
8		cflem	$⊢ A \in On \to \exists x \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))$
9		abn0	$⊢ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \neq \emptyset \leftrightarrow \exists x \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))$
10	8 9	sylibr	$⊢ A \in On \to \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \neq \emptyset$
11		onint	$⊢ (\{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \subseteq On \land \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \neq \emptyset) \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\}$
12	7 10 11	sylancr	$⊢ A \in On \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\}$
13	1 12	eqeltrd	$⊢ A \in On \to cf (A) \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\}$
14		fvex	$⊢ cf (A) \in V$
15		eqeq1	$⊢ x = cf (A) \to (x = card (y) \leftrightarrow cf (A) = card (y))$
16	15	anbi1d	$⊢ x = cf (A) \to ((x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \leftrightarrow (cf (A) = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)))$
17	16	exbidv	$⊢ x = cf (A) \to (\exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \leftrightarrow \exists y (cf (A) = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)))$
18	14 17	elab	$⊢ cf (A) \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \leftrightarrow \exists y (cf (A) = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))$
19	13 18	sylib	$⊢ A \in On \to \exists y (cf (A) = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))$
20		simplr	$⊢ ((A \in On \land cf (A) = card (y)) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to cf (A) = card (y)$
21		onss	$⊢ A \in On \to A \subseteq On$
22		sstr	$⊢ (y \subseteq A \land A \subseteq On) \to y \subseteq On$
23	21 22	sylan2	$⊢ (y \subseteq A \land A \in On) \to y \subseteq On$
24	23	ancoms	$⊢ (A \in On \land y \subseteq A) \to y \subseteq On$
25	24	ad2ant2r	$⊢ ((A \in On \land cf (A) = card (y)) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to y \subseteq On$
26		vex	$⊢ y \in V$
27		onssnum	$⊢ (y \in V \land y \subseteq On) \to y \in dom card$
28	26 27	mpan	$⊢ y \subseteq On \to y \in dom card$
29		cardid2	$⊢ y \in dom card \to card (y) \approx y$
30	28 29	syl	$⊢ y \subseteq On \to card (y) \approx y$
31	30	adantl	$⊢ (cf (A) = card (y) \land y \subseteq On) \to card (y) \approx y$
32		breq1	$⊢ cf (A) = card (y) \to (cf (A) \approx y \leftrightarrow card (y) \approx y)$
33	32	adantr	$⊢ (cf (A) = card (y) \land y \subseteq On) \to (cf (A) \approx y \leftrightarrow card (y) \approx y)$
34	31 33	mpbird	$⊢ (cf (A) = card (y) \land y \subseteq On) \to cf (A) \approx y$
35		bren	$⊢ cf (A) \approx y \leftrightarrow \exists f f : cf (A) \underset{1-1 onto}{⟶} y$
36	34 35	sylib	$⊢ (cf (A) = card (y) \land y \subseteq On) \to \exists f f : cf (A) \underset{1-1 onto}{⟶} y$
37	20 25 36	syl2anc	$⊢ ((A \in On \land cf (A) = card (y)) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to \exists f f : cf (A) \underset{1-1 onto}{⟶} y$
38		f1of1	$⊢ f : cf (A) \underset{1-1 onto}{⟶} y \to f : cf (A) \underset{1-1}{⟶} y$
39		f1ss	$⊢ (f : cf (A) \underset{1-1}{⟶} y \land y \subseteq A) \to f : cf (A) \underset{1-1}{⟶} A$
40	39	ancoms	$⊢ (y \subseteq A \land f : cf (A) \underset{1-1}{⟶} y) \to f : cf (A) \underset{1-1}{⟶} A$
41	38 40	sylan2	$⊢ (y \subseteq A \land f : cf (A) \underset{1-1 onto}{⟶} y) \to f : cf (A) \underset{1-1}{⟶} A$
42	41	adantlr	$⊢ ((y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s) \land f : cf (A) \underset{1-1 onto}{⟶} y) \to f : cf (A) \underset{1-1}{⟶} A$
43	42	3adant1	$⊢ ((A \in On \land cf (A) = card (y)) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s) \land f : cf (A) \underset{1-1 onto}{⟶} y) \to f : cf (A) \underset{1-1}{⟶} A$
44		f1ofo	$⊢ f : cf (A) \underset{1-1 onto}{⟶} y \to f : cf (A) \underset{onto}{⟶} y$
45		foelrn	$⊢ (f : cf (A) \underset{onto}{⟶} y \land s \in y) \to \exists w \in cf (A) s = f (w)$
46		sseq2	$⊢ s = f (w) \to (z \subseteq s \leftrightarrow z \subseteq f (w))$
47	46	biimpcd	$⊢ z \subseteq s \to (s = f (w) \to z \subseteq f (w))$
48	47	reximdv	$⊢ z \subseteq s \to (\exists w \in cf (A) s = f (w) \to \exists w \in cf (A) z \subseteq f (w))$
49	45 48	syl5com	$⊢ (f : cf (A) \underset{onto}{⟶} y \land s \in y) \to (z \subseteq s \to \exists w \in cf (A) z \subseteq f (w))$
50	49	rexlimdva	$⊢ f : cf (A) \underset{onto}{⟶} y \to (\exists s \in y z \subseteq s \to \exists w \in cf (A) z \subseteq f (w))$
51	50	ralimdv	$⊢ f : cf (A) \underset{onto}{⟶} y \to (\forall z \in A \exists s \in y z \subseteq s \to \forall z \in A \exists w \in cf (A) z \subseteq f (w))$
52	44 51	syl	$⊢ f : cf (A) \underset{1-1 onto}{⟶} y \to (\forall z \in A \exists s \in y z \subseteq s \to \forall z \in A \exists w \in cf (A) z \subseteq f (w))$
53	52	impcom	$⊢ (\forall z \in A \exists s \in y z \subseteq s \land f : cf (A) \underset{1-1 onto}{⟶} y) \to \forall z \in A \exists w \in cf (A) z \subseteq f (w)$
54	53	adantll	$⊢ ((y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s) \land f : cf (A) \underset{1-1 onto}{⟶} y) \to \forall z \in A \exists w \in cf (A) z \subseteq f (w)$
55	54	3adant1	$⊢ ((A \in On \land cf (A) = card (y)) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s) \land f : cf (A) \underset{1-1 onto}{⟶} y) \to \forall z \in A \exists w \in cf (A) z \subseteq f (w)$
56	43 55	jca	$⊢ ((A \in On \land cf (A) = card (y)) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s) \land f : cf (A) \underset{1-1 onto}{⟶} y) \to (f : cf (A) \underset{1-1}{⟶} A \land \forall z \in A \exists w \in cf (A) z \subseteq f (w))$
57	56	3expia	$⊢ ((A \in On \land cf (A) = card (y)) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to (f : cf (A) \underset{1-1 onto}{⟶} y \to (f : cf (A) \underset{1-1}{⟶} A \land \forall z \in A \exists w \in cf (A) z \subseteq f (w)))$
58	57	eximdv	$⊢ ((A \in On \land cf (A) = card (y)) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to (\exists f f : cf (A) \underset{1-1 onto}{⟶} y \to \exists f (f : cf (A) \underset{1-1}{⟶} A \land \forall z \in A \exists w \in cf (A) z \subseteq f (w)))$
59	37 58	mpd	$⊢ ((A \in On \land cf (A) = card (y)) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to \exists f (f : cf (A) \underset{1-1}{⟶} A \land \forall z \in A \exists w \in cf (A) z \subseteq f (w))$
60	59	expl	$⊢ A \in On \to ((cf (A) = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to \exists f (f : cf (A) \underset{1-1}{⟶} A \land \forall z \in A \exists w \in cf (A) z \subseteq f (w)))$
61	60	exlimdv	$⊢ A \in On \to (\exists y (cf (A) = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \to \exists f (f : cf (A) \underset{1-1}{⟶} A \land \forall z \in A \exists w \in cf (A) z \subseteq f (w)))$
62	19 61	mpd	$⊢ A \in On \to \exists f (f : cf (A) \underset{1-1}{⟶} A \land \forall z \in A \exists w \in cf (A) z \subseteq f (w))$

Metamath Proof Explorer

Theorem cff1

Proof