coftr

Description: If there is a cofinal map from B to A and another from C to A , then there is also a cofinal map from C to B . Proposition 11.9 of TakeutiZaring p. 102. A limited form of transitivity for the "cof" relation. This is really a lemma for cfcof . (Contributed by Mario Carneiro, 16-Mar-2013)

		Ref	Expression
	Hypothesis	coftr.1	$⊢ H = (t \in C ⟼ ⋂ \{n \in B \| g (t) \subseteq f (n)\})$
	Assertion	coftr	$⊢ \exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to (\exists g (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w)) \to \exists h (h : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq h (w)))$

Proof

Step	Hyp	Ref	Expression
1		coftr.1	$⊢ H = (t \in C ⟼ ⋂ \{n \in B \| g (t) \subseteq f (n)\})$
2		fdm	$⊢ g : C ⟶ A \to dom g = C$
3		vex	$⊢ g \in V$
4	3	dmex	$⊢ dom g \in V$
5	2 4	eqeltrrdi	$⊢ g : C ⟶ A \to C \in V$
6		fveq2	$⊢ t = w \to g (t) = g (w)$
7	6	sseq1d	$⊢ t = w \to (g (t) \subseteq f (n) \leftrightarrow g (w) \subseteq f (n))$
8	7	rabbidv	$⊢ t = w \to \{n \in B \| g (t) \subseteq f (n)\} = \{n \in B \| g (w) \subseteq f (n)\}$
9	8	inteqd	$⊢ t = w \to ⋂ \{n \in B \| g (t) \subseteq f (n)\} = ⋂ \{n \in B \| g (w) \subseteq f (n)\}$
10	9	cbvmptv	$⊢ (t \in C ⟼ ⋂ \{n \in B \| g (t) \subseteq f (n)\}) = (w \in C ⟼ ⋂ \{n \in B \| g (w) \subseteq f (n)\})$
11	1 10	eqtri	$⊢ H = (w \in C ⟼ ⋂ \{n \in B \| g (w) \subseteq f (n)\})$
12		mptexg	$⊢ C \in V \to (w \in C ⟼ ⋂ \{n \in B \| g (w) \subseteq f (n)\}) \in V$
13	11 12	eqeltrid	$⊢ C \in V \to H \in V$
14	5 13	syl	$⊢ g : C ⟶ A \to H \in V$
15	14	ad2antrl	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to H \in V$
16		ffn	$⊢ f : B ⟶ A \to f Fn B$
17		smodm2	$⊢ (f Fn B \land Smo f) \to Ord B$
18	16 17	sylan	$⊢ (f : B ⟶ A \land Smo f) \to Ord B$
19	18	3adant3	$⊢ (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to Ord B$
20	19	adantr	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to Ord B$
21		simpl3	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to \forall x \in A \exists y \in B x \subseteq f (y)$
22		simprl	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to g : C ⟶ A$
23		simpl1	$⊢ ((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to Ord B$
24		simpl2	$⊢ ((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to \forall x \in A \exists y \in B x \subseteq f (y)$
25		ffvelrn	$⊢ (g : C ⟶ A \land w \in C) \to g (w) \in A$
26	25	3ad2antl3	$⊢ ((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to g (w) \in A$
27		sseq1	$⊢ x = g (w) \to (x \subseteq f (y) \leftrightarrow g (w) \subseteq f (y))$
28	27	rexbidv	$⊢ x = g (w) \to (\exists y \in B x \subseteq f (y) \leftrightarrow \exists y \in B g (w) \subseteq f (y))$
29	28	rspccv	$⊢ \forall x \in A \exists y \in B x \subseteq f (y) \to (g (w) \in A \to \exists y \in B g (w) \subseteq f (y))$
30	24 26 29	sylc	$⊢ ((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to \exists y \in B g (w) \subseteq f (y)$
31		ssrab2	$⊢ \{n \in B \| g (w) \subseteq f (n)\} \subseteq B$
32		ordsson	$⊢ Ord B \to B \subseteq On$
33	31 32	sstrid	$⊢ Ord B \to \{n \in B \| g (w) \subseteq f (n)\} \subseteq On$
34		fveq2	$⊢ n = y \to f (n) = f (y)$
35	34	sseq2d	$⊢ n = y \to (g (w) \subseteq f (n) \leftrightarrow g (w) \subseteq f (y))$
36	35	rspcev	$⊢ (y \in B \land g (w) \subseteq f (y)) \to \exists n \in B g (w) \subseteq f (n)$
37		rabn0	$⊢ \{n \in B \| g (w) \subseteq f (n)\} \neq \emptyset \leftrightarrow \exists n \in B g (w) \subseteq f (n)$
38	36 37	sylibr	$⊢ (y \in B \land g (w) \subseteq f (y)) \to \{n \in B \| g (w) \subseteq f (n)\} \neq \emptyset$
39		oninton	$⊢ (\{n \in B \| g (w) \subseteq f (n)\} \subseteq On \land \{n \in B \| g (w) \subseteq f (n)\} \neq \emptyset) \to ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in On$
40	33 38 39	syl2an	$⊢ (Ord B \land (y \in B \land g (w) \subseteq f (y))) \to ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in On$
41		eloni	$⊢ ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in On \to Ord ⋂ \{n \in B \| g (w) \subseteq f (n)\}$
42	40 41	syl	$⊢ (Ord B \land (y \in B \land g (w) \subseteq f (y))) \to Ord ⋂ \{n \in B \| g (w) \subseteq f (n)\}$
43		simpl	$⊢ (Ord B \land (y \in B \land g (w) \subseteq f (y))) \to Ord B$
44	35	intminss	$⊢ (y \in B \land g (w) \subseteq f (y)) \to ⋂ \{n \in B \| g (w) \subseteq f (n)\} \subseteq y$
45	44	adantl	$⊢ (Ord B \land (y \in B \land g (w) \subseteq f (y))) \to ⋂ \{n \in B \| g (w) \subseteq f (n)\} \subseteq y$
46		simprl	$⊢ (Ord B \land (y \in B \land g (w) \subseteq f (y))) \to y \in B$
47		ordtr2	$⊢ (Ord ⋂ \{n \in B \| g (w) \subseteq f (n)\} \land Ord B) \to ((⋂ \{n \in B \| g (w) \subseteq f (n)\} \subseteq y \land y \in B) \to ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in B)$
48	47	imp	$⊢ ((Ord ⋂ \{n \in B \| g (w) \subseteq f (n)\} \land Ord B) \land (⋂ \{n \in B \| g (w) \subseteq f (n)\} \subseteq y \land y \in B)) \to ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in B$
49	42 43 45 46 48	syl22anc	$⊢ (Ord B \land (y \in B \land g (w) \subseteq f (y))) \to ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in B$
50	49	rexlimdvaa	$⊢ Ord B \to (\exists y \in B g (w) \subseteq f (y) \to ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in B)$
51	23 30 50	sylc	$⊢ ((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in B$
52	51 11	fmptd	$⊢ (Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \to H : C ⟶ B$
53	20 21 22 52	syl3anc	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to H : C ⟶ B$
54		simprr	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to \forall z \in A \exists w \in C z \subseteq g (w)$
55		simpl1	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to f : B ⟶ A$
56		ffvelrn	$⊢ (f : B ⟶ A \land s \in B) \to f (s) \in A$
57		sseq1	$⊢ z = f (s) \to (z \subseteq g (w) \leftrightarrow f (s) \subseteq g (w))$
58	57	rexbidv	$⊢ z = f (s) \to (\exists w \in C z \subseteq g (w) \leftrightarrow \exists w \in C f (s) \subseteq g (w))$
59	58	rspccv	$⊢ \forall z \in A \exists w \in C z \subseteq g (w) \to (f (s) \in A \to \exists w \in C f (s) \subseteq g (w))$
60	56 59	syl5	$⊢ \forall z \in A \exists w \in C z \subseteq g (w) \to ((f : B ⟶ A \land s \in B) \to \exists w \in C f (s) \subseteq g (w))$
61	60	expdimp	$⊢ (\forall z \in A \exists w \in C z \subseteq g (w) \land f : B ⟶ A) \to (s \in B \to \exists w \in C f (s) \subseteq g (w))$
62	54 55 61	syl2anc	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to (s \in B \to \exists w \in C f (s) \subseteq g (w))$
63	55 16	syl	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to f Fn B$
64		simpl2	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to Smo f$
65		simpr	$⊢ ((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to w \in C$
66	65 51	jca	$⊢ ((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to (w \in C \land ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in B)$
67	35	elrab	$⊢ y \in \{n \in B \| g (w) \subseteq f (n)\} \leftrightarrow (y \in B \land g (w) \subseteq f (y))$
68		sstr2	$⊢ f (s) \subseteq g (w) \to (g (w) \subseteq f (y) \to f (s) \subseteq f (y))$
69		smoword	$⊢ ((f Fn B \land Smo f) \land (s \in B \land y \in B)) \to (s \subseteq y \leftrightarrow f (s) \subseteq f (y))$
70	69	biimprd	$⊢ ((f Fn B \land Smo f) \land (s \in B \land y \in B)) \to (f (s) \subseteq f (y) \to s \subseteq y)$
71	68 70	syl9r	$⊢ ((f Fn B \land Smo f) \land (s \in B \land y \in B)) \to (f (s) \subseteq g (w) \to (g (w) \subseteq f (y) \to s \subseteq y))$
72	71	expr	$⊢ ((f Fn B \land Smo f) \land s \in B) \to (y \in B \to (f (s) \subseteq g (w) \to (g (w) \subseteq f (y) \to s \subseteq y)))$
73	72	com23	$⊢ ((f Fn B \land Smo f) \land s \in B) \to (f (s) \subseteq g (w) \to (y \in B \to (g (w) \subseteq f (y) \to s \subseteq y)))$
74	73	imp4b	$⊢ (((f Fn B \land Smo f) \land s \in B) \land f (s) \subseteq g (w)) \to ((y \in B \land g (w) \subseteq f (y)) \to s \subseteq y)$
75	67 74	syl5bi	$⊢ (((f Fn B \land Smo f) \land s \in B) \land f (s) \subseteq g (w)) \to (y \in \{n \in B \| g (w) \subseteq f (n)\} \to s \subseteq y)$
76	75	ralrimiv	$⊢ (((f Fn B \land Smo f) \land s \in B) \land f (s) \subseteq g (w)) \to \forall y \in \{n \in B \| g (w) \subseteq f (n)\} s \subseteq y$
77		ssint	$⊢ s \subseteq ⋂ \{n \in B \| g (w) \subseteq f (n)\} \leftrightarrow \forall y \in \{n \in B \| g (w) \subseteq f (n)\} s \subseteq y$
78	76 77	sylibr	$⊢ (((f Fn B \land Smo f) \land s \in B) \land f (s) \subseteq g (w)) \to s \subseteq ⋂ \{n \in B \| g (w) \subseteq f (n)\}$
79	9 1	fvmptg	$⊢ (w \in C \land ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in B) \to H (w) = ⋂ \{n \in B \| g (w) \subseteq f (n)\}$
80	79	sseq2d	$⊢ (w \in C \land ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in B) \to (s \subseteq H (w) \leftrightarrow s \subseteq ⋂ \{n \in B \| g (w) \subseteq f (n)\})$
81	78 80	syl5ibrcom	$⊢ (((f Fn B \land Smo f) \land s \in B) \land f (s) \subseteq g (w)) \to ((w \in C \land ⋂ \{n \in B \| g (w) \subseteq f (n)\} \in B) \to s \subseteq H (w))$
82	66 81	syl5	$⊢ (((f Fn B \land Smo f) \land s \in B) \land f (s) \subseteq g (w)) \to (((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to s \subseteq H (w))$
83	82	ex	$⊢ ((f Fn B \land Smo f) \land s \in B) \to (f (s) \subseteq g (w) \to (((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to s \subseteq H (w)))$
84	83	com23	$⊢ ((f Fn B \land Smo f) \land s \in B) \to (((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land w \in C) \to (f (s) \subseteq g (w) \to s \subseteq H (w)))$
85	84	expdimp	$⊢ (((f Fn B \land Smo f) \land s \in B) \land (Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A)) \to (w \in C \to (f (s) \subseteq g (w) \to s \subseteq H (w)))$
86	85	reximdvai	$⊢ (((f Fn B \land Smo f) \land s \in B) \land (Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A)) \to (\exists w \in C f (s) \subseteq g (w) \to \exists w \in C s \subseteq H (w))$
87	86	ancoms	$⊢ ((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land ((f Fn B \land Smo f) \land s \in B)) \to (\exists w \in C f (s) \subseteq g (w) \to \exists w \in C s \subseteq H (w))$
88	87	expr	$⊢ ((Ord B \land \forall x \in A \exists y \in B x \subseteq f (y) \land g : C ⟶ A) \land (f Fn B \land Smo f)) \to (s \in B \to (\exists w \in C f (s) \subseteq g (w) \to \exists w \in C s \subseteq H (w)))$
89	20 21 22 63 64 88	syl32anc	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to (s \in B \to (\exists w \in C f (s) \subseteq g (w) \to \exists w \in C s \subseteq H (w)))$
90	62 89	mpdd	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to (s \in B \to \exists w \in C s \subseteq H (w))$
91	90	ralrimiv	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to \forall s \in B \exists w \in C s \subseteq H (w)$
92		feq1	$⊢ h = H \to (h : C ⟶ B \leftrightarrow H : C ⟶ B)$
93		fveq1	$⊢ h = H \to h (w) = H (w)$
94	93	sseq2d	$⊢ h = H \to (s \subseteq h (w) \leftrightarrow s \subseteq H (w))$
95	94	rexbidv	$⊢ h = H \to (\exists w \in C s \subseteq h (w) \leftrightarrow \exists w \in C s \subseteq H (w))$
96	95	ralbidv	$⊢ h = H \to (\forall s \in B \exists w \in C s \subseteq h (w) \leftrightarrow \forall s \in B \exists w \in C s \subseteq H (w))$
97	92 96	anbi12d	$⊢ h = H \to ((h : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq h (w)) \leftrightarrow (H : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq H (w)))$
98	97	spcegv	$⊢ H \in V \to ((H : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq H (w)) \to \exists h (h : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq h (w)))$
99	98	3impib	$⊢ (H \in V \land H : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq H (w)) \to \exists h (h : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq h (w))$
100	15 53 91 99	syl3anc	$⊢ ((f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \land (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w))) \to \exists h (h : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq h (w))$
101	100	ex	$⊢ (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to ((g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w)) \to \exists h (h : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq h (w)))$
102	101	exlimdv	$⊢ (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to (\exists g (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w)) \to \exists h (h : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq h (w)))$
103	102	exlimiv	$⊢ \exists f (f : B ⟶ A \land Smo f \land \forall x \in A \exists y \in B x \subseteq f (y)) \to (\exists g (g : C ⟶ A \land \forall z \in A \exists w \in C z \subseteq g (w)) \to \exists h (h : C ⟶ B \land \forall s \in B \exists w \in C s \subseteq h (w)))$

Metamath Proof Explorer

Theorem coftr

Proof