cfcoflem

Description: Lemma for cfcof , showing subset relation in one direction. (Contributed by Mario Carneiro, 9-Mar-2013) (Revised by Mario Carneiro, 26-Dec-2014)

		Ref	Expression
	Assertion	cfcoflem	$⊢ (A \in On \land B \in On) \to (\exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to cf (A) \subseteq cf (B))$

Proof

Step	Hyp	Ref	Expression
1		cff1	$⊢ B \in On \to \exists g (g : cf (B) \underset{1-1}{⟶} B \land \forall y \in B \exists z \in cf (B) y \subseteq g (z))$
2		f1f	$⊢ g : cf (B) \underset{1-1}{⟶} B \to g : cf (B) ⟶ B$
3		fco	$⊢ (f : B ⟶ A \land g : cf (B) ⟶ B) \to (f \circ g) : cf (B) ⟶ A$
4	3	adantlr	$⊢ ((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to (f \circ g) : cf (B) ⟶ A$
5		r19.29	$⊢ (\forall y \in B \exists z \in cf (B) y \subseteq g (z) \land \exists y \in B x \subseteq f (y)) \to \exists y \in B (\exists z \in cf (B) y \subseteq g (z) \land x \subseteq f (y))$
6		ffvelrn	$⊢ (g : cf (B) ⟶ B \land z \in cf (B)) \to g (z) \in B$
7		ffn	$⊢ f : B ⟶ A \to f Fn B$
8		smoword	$⊢ ((f Fn B \land Smo f) \land (y \in B \land g (z) \in B)) \to (y \subseteq g (z) \leftrightarrow f (y) \subseteq f (g (z)))$
9	8	biimpd	$⊢ ((f Fn B \land Smo f) \land (y \in B \land g (z) \in B)) \to (y \subseteq g (z) \to f (y) \subseteq f (g (z)))$
10	9	exp32	$⊢ (f Fn B \land Smo f) \to (y \in B \to (g (z) \in B \to (y \subseteq g (z) \to f (y) \subseteq f (g (z)))))$
11	7 10	sylan	$⊢ (f : B ⟶ A \land Smo f) \to (y \in B \to (g (z) \in B \to (y \subseteq g (z) \to f (y) \subseteq f (g (z)))))$
12	6 11	syl7	$⊢ (f : B ⟶ A \land Smo f) \to (y \in B \to ((g : cf (B) ⟶ B \land z \in cf (B)) \to (y \subseteq g (z) \to f (y) \subseteq f (g (z)))))$
13	12	com23	$⊢ (f : B ⟶ A \land Smo f) \to ((g : cf (B) ⟶ B \land z \in cf (B)) \to (y \in B \to (y \subseteq g (z) \to f (y) \subseteq f (g (z)))))$
14	13	expdimp	$⊢ ((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to (z \in cf (B) \to (y \in B \to (y \subseteq g (z) \to f (y) \subseteq f (g (z)))))$
15	14	3imp2	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land (z \in cf (B) \land y \in B \land y \subseteq g (z))) \to f (y) \subseteq f (g (z))$
16		sstr2	$⊢ x \subseteq f (y) \to (f (y) \subseteq f (g (z)) \to x \subseteq f (g (z)))$
17	15 16	syl5com	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land (z \in cf (B) \land y \in B \land y \subseteq g (z))) \to (x \subseteq f (y) \to x \subseteq f (g (z)))$
18		fvco3	$⊢ (g : cf (B) ⟶ B \land z \in cf (B)) \to (f \circ g) (z) = f (g (z))$
19	18	sseq2d	$⊢ (g : cf (B) ⟶ B \land z \in cf (B)) \to (x \subseteq (f \circ g) (z) \leftrightarrow x \subseteq f (g (z)))$
20	19	adantll	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land z \in cf (B)) \to (x \subseteq (f \circ g) (z) \leftrightarrow x \subseteq f (g (z)))$
21	20	3ad2antr1	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land (z \in cf (B) \land y \in B \land y \subseteq g (z))) \to (x \subseteq (f \circ g) (z) \leftrightarrow x \subseteq f (g (z)))$
22	17 21	sylibrd	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land (z \in cf (B) \land y \in B \land y \subseteq g (z))) \to (x \subseteq f (y) \to x \subseteq (f \circ g) (z))$
23	22	expcom	$⊢ (z \in cf (B) \land y \in B \land y \subseteq g (z)) \to (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to (x \subseteq f (y) \to x \subseteq (f \circ g) (z)))$
24	23	3expia	$⊢ (z \in cf (B) \land y \in B) \to (y \subseteq g (z) \to (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to (x \subseteq f (y) \to x \subseteq (f \circ g) (z))))$
25	24	com4t	$⊢ ((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to (x \subseteq f (y) \to ((z \in cf (B) \land y \in B) \to (y \subseteq g (z) \to x \subseteq (f \circ g) (z))))$
26	25	imp	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land x \subseteq f (y)) \to ((z \in cf (B) \land y \in B) \to (y \subseteq g (z) \to x \subseteq (f \circ g) (z)))$
27	26	expcomd	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land x \subseteq f (y)) \to (y \in B \to (z \in cf (B) \to (y \subseteq g (z) \to x \subseteq (f \circ g) (z))))$
28	27	imp31	$⊢ (((((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land x \subseteq f (y)) \land y \in B) \land z \in cf (B)) \to (y \subseteq g (z) \to x \subseteq (f \circ g) (z))$
29	28	reximdva	$⊢ ((((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land x \subseteq f (y)) \land y \in B) \to (\exists z \in cf (B) y \subseteq g (z) \to \exists z \in cf (B) x \subseteq (f \circ g) (z))$
30	29	exp31	$⊢ ((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to (x \subseteq f (y) \to (y \in B \to (\exists z \in cf (B) y \subseteq g (z) \to \exists z \in cf (B) x \subseteq (f \circ g) (z))))$
31	30	com34	$⊢ ((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to (x \subseteq f (y) \to (\exists z \in cf (B) y \subseteq g (z) \to (y \in B \to \exists z \in cf (B) x \subseteq (f \circ g) (z))))$
32	31	impcomd	$⊢ ((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to ((\exists z \in cf (B) y \subseteq g (z) \land x \subseteq f (y)) \to (y \in B \to \exists z \in cf (B) x \subseteq (f \circ g) (z)))$
33	32	com23	$⊢ ((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to (y \in B \to ((\exists z \in cf (B) y \subseteq g (z) \land x \subseteq f (y)) \to \exists z \in cf (B) x \subseteq (f \circ g) (z)))$
34	33	rexlimdv	$⊢ ((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to (\exists y \in B (\exists z \in cf (B) y \subseteq g (z) \land x \subseteq f (y)) \to \exists z \in cf (B) x \subseteq (f \circ g) (z))$
35	5 34	syl5	$⊢ ((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \to ((\forall y \in B \exists z \in cf (B) y \subseteq g (z) \land \exists y \in B x \subseteq f (y)) \to \exists z \in cf (B) x \subseteq (f \circ g) (z))$
36	35	expdimp	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land \forall y \in B \exists z \in cf (B) y \subseteq g (z)) \to (\exists y \in B x \subseteq f (y) \to \exists z \in cf (B) x \subseteq (f \circ g) (z))$
37	36	ralimdv	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land \forall y \in B \exists z \in cf (B) y \subseteq g (z)) \to (\forall x \in A \exists y \in B x \subseteq f (y) \to \forall x \in A \exists z \in cf (B) x \subseteq (f \circ g) (z))$
38	37	impr	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land (\forall y \in B \exists z \in cf (B) y \subseteq g (z) \land \forall x \in A \exists y \in B x \subseteq f (y))) \to \forall x \in A \exists z \in cf (B) x \subseteq (f \circ g) (z)$
39		vex	$⊢ f \in V$
40		vex	$⊢ g \in V$
41	39 40	coex	$⊢ f \circ g \in V$
42		feq1	$⊢ h = f \circ g \to (h : cf (B) ⟶ A \leftrightarrow (f \circ g) : cf (B) ⟶ A)$
43		fveq1	$⊢ h = f \circ g \to h (z) = (f \circ g) (z)$
44	43	sseq2d	$⊢ h = f \circ g \to (x \subseteq h (z) \leftrightarrow x \subseteq (f \circ g) (z))$
45	44	rexbidv	$⊢ h = f \circ g \to (\exists z \in cf (B) x \subseteq h (z) \leftrightarrow \exists z \in cf (B) x \subseteq (f \circ g) (z))$
46	45	ralbidv	$⊢ h = f \circ g \to (\forall x \in A \exists z \in cf (B) x \subseteq h (z) \leftrightarrow \forall x \in A \exists z \in cf (B) x \subseteq (f \circ g) (z))$
47	42 46	anbi12d	$⊢ h = f \circ g \to ((h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z)) \leftrightarrow ((f \circ g) : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq (f \circ g) (z)))$
48	41 47	spcev	$⊢ ((f \circ g) : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq (f \circ g) (z)) \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z))$
49	4 38 48	syl2an2r	$⊢ (((f : B ⟶ A \land Smo f) \land g : cf (B) ⟶ B) \land (\forall y \in B \exists z \in cf (B) y \subseteq g (z) \land \forall x \in A \exists y \in B x \subseteq f (y))) \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z))$
50	49	exp43	$⊢ (f : B ⟶ A \land Smo f) \to (g : cf (B) ⟶ B \to (\forall y \in B \exists z \in cf (B) y \subseteq g (z) \to (\forall x \in A \exists y \in B x \subseteq f (y) \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z)))))$
51	50	com24	$⊢ (f : B ⟶ A \land Smo f) \to (\forall x \in A \exists y \in B x \subseteq f (y) \to (\forall y \in B \exists z \in cf (B) y \subseteq g (z) \to (g : cf (B) ⟶ B \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z)))))$
52	51	3impia	$⊢ (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to (\forall y \in B \exists z \in cf (B) y \subseteq g (z) \to (g : cf (B) ⟶ B \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z))))$
53	52	exlimiv	$⊢ \exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to (\forall y \in B \exists z \in cf (B) y \subseteq g (z) \to (g : cf (B) ⟶ B \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z))))$
54	53	com13	$⊢ g : cf (B) ⟶ B \to (\forall y \in B \exists z \in cf (B) y \subseteq g (z) \to (\exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z))))$
55	2 54	syl	$⊢ g : cf (B) \underset{1-1}{⟶} B \to (\forall y \in B \exists z \in cf (B) y \subseteq g (z) \to (\exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z))))$
56	55	imp	$⊢ (g : cf (B) \underset{1-1}{⟶} B \land \forall y \in B \exists z \in cf (B) y \subseteq g (z)) \to (\exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z)))$
57	56	exlimiv	$⊢ \exists g (g : cf (B) \underset{1-1}{⟶} B \land \forall y \in B \exists z \in cf (B) y \subseteq g (z)) \to (\exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z)))$
58	1 57	syl	$⊢ B \in On \to (\exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to \exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z)))$
59		cfon	$⊢ cf (B) \in On$
60		cfflb	$⊢ (A \in On \land cf (B) \in On) \to (\exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z)) \to cf (A) \subseteq cf (B))$
61	59 60	mpan2	$⊢ A \in On \to (\exists h (h : cf (B) ⟶ A \land \forall x \in A \exists z \in cf (B) x \subseteq h (z)) \to cf (A) \subseteq cf (B))$
62	58 61	sylan9r	$⊢ (A \in On \land B \in On) \to (\exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to cf (A) \subseteq cf (B))$

Metamath Proof Explorer

Theorem cfcoflem

Proof