cfflb

Description: If there is a cofinal map from B to A , then B is at least ( cfA ) . This theorem and cff1 motivate the picture of ( cfA ) as the greatest lower bound of the domain of cofinal maps into A . (Contributed by Mario Carneiro, 28-Feb-2013)

		Ref	Expression
	Assertion	cfflb	$⊢ (A \in On \land B \in On) \to (\exists f (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w)) \to cf (A) \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		frn	$⊢ f : B ⟶ A \to ran f \subseteq A$
2	1	adantr	$⊢ (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w)) \to ran f \subseteq A$
3		ffn	$⊢ f : B ⟶ A \to f Fn B$
4		fnfvelrn	$⊢ (f Fn B \land w \in B) \to f (w) \in ran f$
5	3 4	sylan	$⊢ (f : B ⟶ A \land w \in B) \to f (w) \in ran f$
6		sseq2	$⊢ s = f (w) \to (z \subseteq s \leftrightarrow z \subseteq f (w))$
7	6	rspcev	$⊢ (f (w) \in ran f \land z \subseteq f (w)) \to \exists s \in ran f z \subseteq s$
8	5 7	sylan	$⊢ ((f : B ⟶ A \land w \in B) \land z \subseteq f (w)) \to \exists s \in ran f z \subseteq s$
9	8	rexlimdva2	$⊢ f : B ⟶ A \to (\exists w \in B z \subseteq f (w) \to \exists s \in ran f z \subseteq s)$
10	9	ralimdv	$⊢ f : B ⟶ A \to (\forall z \in A \exists w \in B z \subseteq f (w) \to \forall z \in A \exists s \in ran f z \subseteq s)$
11	10	imp	$⊢ (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w)) \to \forall z \in A \exists s \in ran f z \subseteq s$
12	2 11	jca	$⊢ (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w)) \to (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)$
13		fvex	$⊢ card (ran f) \in V$
14		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))\}$
15	14	adantr	$⊢ (A \in On \land B \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))\}$
16	15	3ad2ant2	$⊢ (x = card (ran f) \land (A \in On \land B \in On) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)) \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))\}$
17		vex	$⊢ f \in V$
18	17	rnex	$⊢ ran f \in V$
19		fveq2	$⊢ y = ran f \to card (y) = card (ran f)$
20	19	eqeq2d	$⊢ y = ran f \to (x = card (y) \leftrightarrow x = card (ran f))$
21		sseq1	$⊢ y = ran f \to (y \subseteq A \leftrightarrow ran f \subseteq A)$
22		rexeq	$⊢ y = ran f \to (\exists s \in y z \subseteq s \leftrightarrow \exists s \in ran f z \subseteq s)$
23	22	ralbidv	$⊢ y = ran f \to (\forall z \in A \exists s \in y z \subseteq s \leftrightarrow \forall z \in A \exists s \in ran f z \subseteq s)$
24	21 23	anbi12d	$⊢ y = ran f \to ((y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s) \leftrightarrow (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s))$
25	20 24	anbi12d	$⊢ y = ran f \to ((x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s)) \leftrightarrow (x = card (ran f) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)))$
26	18 25	spcev	$⊢ (x = card (ran f) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)) \to \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))$
27		abid	$⊢ x \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 (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))$
28	26 27	sylibr	$⊢ (x = card (ran f) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)) \to x \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\}$
29		intss1	$⊢ x \in \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \subseteq x$
30	28 29	syl	$⊢ (x = card (ran f) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)) \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \subseteq x$
31	30	3adant2	$⊢ (x = card (ran f) \land (A \in On \land B \in On) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)) \to ⋂ \{x \| \exists y (x = card (y) \land (y \subseteq A \land \forall z \in A \exists s \in y z \subseteq s))\} \subseteq x$
32	16 31	eqsstrd	$⊢ (x = card (ran f) \land (A \in On \land B \in On) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)) \to cf (A) \subseteq x$
33	32	3expib	$⊢ x = card (ran f) \to (((A \in On \land B \in On) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)) \to cf (A) \subseteq x)$
34		sseq2	$⊢ x = card (ran f) \to (cf (A) \subseteq x \leftrightarrow cf (A) \subseteq card (ran f))$
35	33 34	sylibd	$⊢ x = card (ran f) \to (((A \in On \land B \in On) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)) \to cf (A) \subseteq card (ran f))$
36	13 35	vtocle	$⊢ ((A \in On \land B \in On) \land (ran f \subseteq A \land \forall z \in A \exists s \in ran f z \subseteq s)) \to cf (A) \subseteq card (ran f)$
37	12 36	sylan2	$⊢ ((A \in On \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to cf (A) \subseteq card (ran f)$
38		cardidm	$⊢ card (card (ran f)) = card (ran f)$
39		onss	$⊢ A \in On \to A \subseteq On$
40	1 39	sylan9ssr	$⊢ (A \in On \land f : B ⟶ A) \to ran f \subseteq On$
41	40	3adant2	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to ran f \subseteq On$
42		onssnum	$⊢ (ran f \in V \land ran f \subseteq On) \to ran f \in dom card$
43	18 41 42	sylancr	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to ran f \in dom card$
44		cardid2	$⊢ ran f \in dom card \to card (ran f) \approx ran f$
45	43 44	syl	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to card (ran f) \approx ran f$
46		onenon	$⊢ B \in On \to B \in dom card$
47		dffn4	$⊢ f Fn B \leftrightarrow f : B \underset{onto}{⟶} ran f$
48	3 47	sylib	$⊢ f : B ⟶ A \to f : B \underset{onto}{⟶} ran f$
49		fodomnum	$⊢ B \in dom card \to (f : B \underset{onto}{⟶} ran f \to ran f ≼ B)$
50	46 48 49	syl2im	$⊢ B \in On \to (f : B ⟶ A \to ran f ≼ B)$
51	50	imp	$⊢ (B \in On \land f : B ⟶ A) \to ran f ≼ B$
52	51	3adant1	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to ran f ≼ B$
53		endomtr	$⊢ (card (ran f) \approx ran f \land ran f ≼ B) \to card (ran f) ≼ B$
54	45 52 53	syl2anc	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to card (ran f) ≼ B$
55		cardon	$⊢ card (ran f) \in On$
56		onenon	$⊢ card (ran f) \in On \to card (ran f) \in dom card$
57	55 56	ax-mp	$⊢ card (ran f) \in dom card$
58		carddom2	$⊢ (card (ran f) \in dom card \land B \in dom card) \to (card (card (ran f)) \subseteq card (B) \leftrightarrow card (ran f) ≼ B)$
59	57 46 58	sylancr	$⊢ B \in On \to (card (card (ran f)) \subseteq card (B) \leftrightarrow card (ran f) ≼ B)$
60	59	3ad2ant2	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to (card (card (ran f)) \subseteq card (B) \leftrightarrow card (ran f) ≼ B)$
61	54 60	mpbird	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to card (card (ran f)) \subseteq card (B)$
62		cardonle	$⊢ B \in On \to card (B) \subseteq B$
63	62	3ad2ant2	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to card (B) \subseteq B$
64	61 63	sstrd	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to card (card (ran f)) \subseteq B$
65	38 64	eqsstrrid	$⊢ (A \in On \land B \in On \land f : B ⟶ A) \to card (ran f) \subseteq B$
66	65	3expa	$⊢ ((A \in On \land B \in On) \land f : B ⟶ A) \to card (ran f) \subseteq B$
67	66	adantrr	$⊢ ((A \in On \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to card (ran f) \subseteq B$
68	37 67	sstrd	$⊢ ((A \in On \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to cf (A) \subseteq B$
69	68	ex	$⊢ (A \in On \land B \in On) \to ((f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w)) \to cf (A) \subseteq B)$
70	69	exlimdv	$⊢ (A \in On \land B \in On) \to (\exists f (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w)) \to cf (A) \subseteq B)$

Metamath Proof Explorer

Theorem cfflb

Proof