cofsmo

Description: Any cofinal map implies the existence of a strictly monotone cofinal map with a domain no larger than the original. Proposition 11.7 of TakeutiZaring p. 101. (Contributed by Mario Carneiro, 20-Mar-2013)

	Ref	Expression
Hypotheses	cofsmo.1	$⊢ C = \{y \in B \| \forall w \in y f (w) \in f (y)\}$
	cofsmo.2	$⊢ K = ⋂ \{x \in B \| z \subseteq f (x)\}$
	cofsmo.3	$⊢ O = OrdIso (E, C)$
Assertion	cofsmo	$⊢ (Ord A \land B \in On) \to (\exists f (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w)) \to \exists x \in suc B \exists g (g : x ⟶ A \land Smo g \land \forall z \in A \exists v \in x z \subseteq g (v)))$

Proof

Step	Hyp	Ref	Expression
1		cofsmo.1	$⊢ C = \{y \in B \| \forall w \in y f (w) \in f (y)\}$
2		cofsmo.2	$⊢ K = ⋂ \{x \in B \| z \subseteq f (x)\}$
3		cofsmo.3	$⊢ O = OrdIso (E, C)$
4	1	ssrab3	$⊢ C \subseteq B$
5		ssexg	$⊢ (C \subseteq B \land B \in On) \to C \in V$
6	4 5	mpan	$⊢ B \in On \to C \in V$
7		onss	$⊢ B \in On \to B \subseteq On$
8	4 7	sstrid	$⊢ B \in On \to C \subseteq On$
9		epweon	$⊢ E We On$
10		wess	$⊢ C \subseteq On \to (E We On \to E We C)$
11	8 9 10	mpisyl	$⊢ B \in On \to E We C$
12	3	oiiso	$⊢ (C \in V \land E We C) \to O {Isom}_{E, E} (dom O, C)$
13	6 11 12	syl2anc	$⊢ B \in On \to O {Isom}_{E, E} (dom O, C)$
14	13	ad2antlr	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to O {Isom}_{E, E} (dom O, C)$
15		isof1o	$⊢ O {Isom}_{E, E} (dom O, C) \to O : dom O \underset{1-1 onto}{⟶} C$
16		f1ofo	$⊢ O : dom O \underset{1-1 onto}{⟶} C \to O : dom O \underset{onto}{⟶} C$
17	14 15 16	3syl	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to O : dom O \underset{onto}{⟶} C$
18		fof	$⊢ O : dom O \underset{onto}{⟶} C \to O : dom O ⟶ C$
19		fss	$⊢ (O : dom O ⟶ C \land C \subseteq B) \to O : dom O ⟶ B$
20	18 4 19	sylancl	$⊢ O : dom O \underset{onto}{⟶} C \to O : dom O ⟶ B$
21	17 20	syl	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to O : dom O ⟶ B$
22	3	oion	$⊢ C \in V \to dom O \in On$
23	6 22	syl	$⊢ B \in On \to dom O \in On$
24	23	ad2antlr	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to dom O \in On$
25		simplr	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to B \in On$
26		eloni	$⊢ dom O \in On \to Ord dom O$
27		smoiso2	$⊢ (Ord dom O \land C \subseteq On) \to ((O : dom O \underset{onto}{⟶} C \land Smo O) \leftrightarrow O {Isom}_{E, E} (dom O, C))$
28	26 8 27	syl2an	$⊢ (dom O \in On \land B \in On) \to ((O : dom O \underset{onto}{⟶} C \land Smo O) \leftrightarrow O {Isom}_{E, E} (dom O, C))$
29	28	biimpar	$⊢ ((dom O \in On \land B \in On) \land O {Isom}_{E, E} (dom O, C)) \to (O : dom O \underset{onto}{⟶} C \land Smo O)$
30	29	simprd	$⊢ ((dom O \in On \land B \in On) \land O {Isom}_{E, E} (dom O, C)) \to Smo O$
31	24 25 14 30	syl21anc	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to Smo O$
32		eloni	$⊢ B \in On \to Ord B$
33	32	ad2antlr	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to Ord B$
34		smorndom	$⊢ (O : dom O ⟶ B \land Smo O \land Ord B) \to dom O \subseteq B$
35	21 31 33 34	syl3anc	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to dom O \subseteq B$
36		onsssuc	$⊢ (dom O \in On \land B \in On) \to (dom O \subseteq B \leftrightarrow dom O \in suc B)$
37	24 25 36	syl2anc	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to (dom O \subseteq B \leftrightarrow dom O \in suc B)$
38	35 37	mpbid	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to dom O \in suc B$
39	38	adantrr	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to dom O \in suc B$
40		vex	$⊢ f \in V$
41	3	oiexg	$⊢ C \in V \to O \in V$
42	6 41	syl	$⊢ B \in On \to O \in V$
43	42	ad2antlr	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to O \in V$
44		coexg	$⊢ (f \in V \land O \in V) \to f \circ O \in V$
45	40 43 44	sylancr	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to f \circ O \in V$
46		simprl	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to f : B ⟶ A$
47	21	adantrr	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to O : dom O ⟶ B$
48		fco	$⊢ (f : B ⟶ A \land O : dom O ⟶ B) \to (f \circ O) : dom O ⟶ A$
49	46 47 48	syl2anc	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to (f \circ O) : dom O ⟶ A$
50		simpr	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to f : B ⟶ A$
51	50 21 48	syl2anc	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to (f \circ O) : dom O ⟶ A$
52		ordsson	$⊢ Ord A \to A \subseteq On$
53	52	ad2antrr	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to A \subseteq On$
54	24 26	syl	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to Ord dom O$
55	17 18	syl	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to O : dom O ⟶ C$
56		simpl	$⊢ (s \in dom O \land t \in s) \to s \in dom O$
57		ffvelrn	$⊢ (O : dom O ⟶ C \land s \in dom O) \to O (s) \in C$
58	55 56 57	syl2an	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land (s \in dom O \land t \in s)) \to O (s) \in C$
59		ffn	$⊢ O : dom O ⟶ C \to O Fn dom O$
60	17 18 59	3syl	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to O Fn dom O$
61	60 31	jca	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to (O Fn dom O \land Smo O)$
62		smoel2	$⊢ ((O Fn dom O \land Smo O) \land (s \in dom O \land t \in s)) \to O (t) \in O (s)$
63	61 62	sylan	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land (s \in dom O \land t \in s)) \to O (t) \in O (s)$
64		fveq2	$⊢ z = O (s) \to f (z) = f (O (s))$
65	64	eleq2d	$⊢ z = O (s) \to (f (x) \in f (z) \leftrightarrow f (x) \in f (O (s)))$
66	65	raleqbi1dv	$⊢ z = O (s) \to (\forall x \in z f (x) \in f (z) \leftrightarrow \forall x \in O (s) f (x) \in f (O (s)))$
67		fveq2	$⊢ w = x \to f (w) = f (x)$
68	67	eleq1d	$⊢ w = x \to (f (w) \in f (y) \leftrightarrow f (x) \in f (y))$
69	68	cbvralvw	$⊢ \forall w \in y f (w) \in f (y) \leftrightarrow \forall x \in y f (x) \in f (y)$
70		fveq2	$⊢ y = z \to f (y) = f (z)$
71	70	eleq2d	$⊢ y = z \to (f (x) \in f (y) \leftrightarrow f (x) \in f (z))$
72	71	raleqbi1dv	$⊢ y = z \to (\forall x \in y f (x) \in f (y) \leftrightarrow \forall x \in z f (x) \in f (z))$
73	69 72	syl5bb	$⊢ y = z \to (\forall w \in y f (w) \in f (y) \leftrightarrow \forall x \in z f (x) \in f (z))$
74	73	cbvrabv	$⊢ \{y \in B \| \forall w \in y f (w) \in f (y)\} = \{z \in B \| \forall x \in z f (x) \in f (z)\}$
75	1 74	eqtri	$⊢ C = \{z \in B \| \forall x \in z f (x) \in f (z)\}$
76	66 75	elrab2	$⊢ O (s) \in C \leftrightarrow (O (s) \in B \land \forall x \in O (s) f (x) \in f (O (s)))$
77	76	simprbi	$⊢ O (s) \in C \to \forall x \in O (s) f (x) \in f (O (s))$
78		fveq2	$⊢ x = O (t) \to f (x) = f (O (t))$
79	78	eleq1d	$⊢ x = O (t) \to (f (x) \in f (O (s)) \leftrightarrow f (O (t)) \in f (O (s)))$
80	79	rspccv	$⊢ \forall x \in O (s) f (x) \in f (O (s)) \to (O (t) \in O (s) \to f (O (t)) \in f (O (s)))$
81	77 80	syl	$⊢ O (s) \in C \to (O (t) \in O (s) \to f (O (t)) \in f (O (s)))$
82	58 63 81	sylc	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land (s \in dom O \land t \in s)) \to f (O (t)) \in f (O (s))$
83		ordtr1	$⊢ Ord dom O \to ((t \in s \land s \in dom O) \to t \in dom O)$
84	83	ancomsd	$⊢ Ord dom O \to ((s \in dom O \land t \in s) \to t \in dom O)$
85	24 26 84	3syl	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to ((s \in dom O \land t \in s) \to t \in dom O)$
86	85	imp	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land (s \in dom O \land t \in s)) \to t \in dom O$
87		fvco3	$⊢ (O : dom O ⟶ B \land t \in dom O) \to (f \circ O) (t) = f (O (t))$
88	21 86 87	syl2an2r	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land (s \in dom O \land t \in s)) \to (f \circ O) (t) = f (O (t))$
89		simprl	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land (s \in dom O \land t \in s)) \to s \in dom O$
90		fvco3	$⊢ (O : dom O ⟶ B \land s \in dom O) \to (f \circ O) (s) = f (O (s))$
91	21 89 90	syl2an2r	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land (s \in dom O \land t \in s)) \to (f \circ O) (s) = f (O (s))$
92	82 88 91	3eltr4d	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land (s \in dom O \land t \in s)) \to (f \circ O) (t) \in (f \circ O) (s)$
93	92	ralrimivva	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to \forall s \in dom O \forall t \in s (f \circ O) (t) \in (f \circ O) (s)$
94		issmo2	$⊢ (f \circ O) : dom O ⟶ A \to ((A \subseteq On \land Ord dom O \land \forall s \in dom O \forall t \in s (f \circ O) (t) \in (f \circ O) (s)) \to Smo (f \circ O))$
95	94	imp	$⊢ ((f \circ O) : dom O ⟶ A \land (A \subseteq On \land Ord dom O \land \forall s \in dom O \forall t \in s (f \circ O) (t) \in (f \circ O) (s))) \to Smo (f \circ O)$
96	51 53 54 93 95	syl13anc	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to Smo (f \circ O)$
97	96	adantrr	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to Smo (f \circ O)$
98		rabn0	$⊢ \{w \in B \| z \subseteq f (w)\} \neq \emptyset \leftrightarrow \exists w \in B z \subseteq f (w)$
99		ssrab2	$⊢ \{w \in B \| z \subseteq f (w)\} \subseteq B$
100	99 7	sstrid	$⊢ B \in On \to \{w \in B \| z \subseteq f (w)\} \subseteq On$
101		fveq2	$⊢ x = w \to f (x) = f (w)$
102	101	sseq2d	$⊢ x = w \to (z \subseteq f (x) \leftrightarrow z \subseteq f (w))$
103	102	cbvrabv	$⊢ \{x \in B \| z \subseteq f (x)\} = \{w \in B \| z \subseteq f (w)\}$
104	103	inteqi	$⊢ ⋂ \{x \in B \| z \subseteq f (x)\} = ⋂ \{w \in B \| z \subseteq f (w)\}$
105	2 104	eqtri	$⊢ K = ⋂ \{w \in B \| z \subseteq f (w)\}$
106		onint	$⊢ (\{w \in B \| z \subseteq f (w)\} \subseteq On \land \{w \in B \| z \subseteq f (w)\} \neq \emptyset) \to ⋂ \{w \in B \| z \subseteq f (w)\} \in \{w \in B \| z \subseteq f (w)\}$
107	105 106	eqeltrid	$⊢ (\{w \in B \| z \subseteq f (w)\} \subseteq On \land \{w \in B \| z \subseteq f (w)\} \neq \emptyset) \to K \in \{w \in B \| z \subseteq f (w)\}$
108	100 107	sylan	$⊢ (B \in On \land \{w \in B \| z \subseteq f (w)\} \neq \emptyset) \to K \in \{w \in B \| z \subseteq f (w)\}$
109	98 108	sylan2br	$⊢ (B \in On \land \exists w \in B z \subseteq f (w)) \to K \in \{w \in B \| z \subseteq f (w)\}$
110		fveq2	$⊢ w = K \to f (w) = f (K)$
111	110	sseq2d	$⊢ w = K \to (z \subseteq f (w) \leftrightarrow z \subseteq f (K))$
112	111	elrab	$⊢ K \in \{w \in B \| z \subseteq f (w)\} \leftrightarrow (K \in B \land z \subseteq f (K))$
113	109 112	sylib	$⊢ (B \in On \land \exists w \in B z \subseteq f (w)) \to (K \in B \land z \subseteq f (K))$
114	113	ex	$⊢ B \in On \to (\exists w \in B z \subseteq f (w) \to (K \in B \land z \subseteq f (K)))$
115	114	adantl	$⊢ (Ord A \land B \in On) \to (\exists w \in B z \subseteq f (w) \to (K \in B \land z \subseteq f (K)))$
116		simpr2	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K))) \to K \in B$
117		simp3	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to w \in K$
118	105	eleq2i	$⊢ w \in K \leftrightarrow w \in ⋂ \{w \in B \| z \subseteq f (w)\}$
119		simp21	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to f : B ⟶ A$
120		simp1l	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to Ord A$
121	120 52	syl	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to A \subseteq On$
122	119 121	fssd	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to f : B ⟶ On$
123		simp22	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to K \in B$
124	122 123	ffvelrnd	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to f (K) \in On$
125		simp1r	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to B \in On$
126		ontr1	$⊢ B \in On \to ((w \in K \land K \in B) \to w \in B)$
127	126	3impib	$⊢ (B \in On \land w \in K \land K \in B) \to w \in B$
128	125 117 123 127	syl3anc	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to w \in B$
129	122 128	ffvelrnd	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to f (w) \in On$
130		ontri1	$⊢ (f (K) \in On \land f (w) \in On) \to (f (K) \subseteq f (w) \leftrightarrow \neg f (w) \in f (K))$
131	124 129 130	syl2anc	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to (f (K) \subseteq f (w) \leftrightarrow \neg f (w) \in f (K))$
132		simp23	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to z \subseteq f (K)$
133		simpl1	$⊢ ((B \in On \land w \in K \land K \in B) \land (z \subseteq f (K) \land f (K) \subseteq f (w))) \to B \in On$
134	133 100	syl	$⊢ ((B \in On \land w \in K \land K \in B) \land (z \subseteq f (K) \land f (K) \subseteq f (w))) \to \{w \in B \| z \subseteq f (w)\} \subseteq On$
135		sstr	$⊢ (z \subseteq f (K) \land f (K) \subseteq f (w)) \to z \subseteq f (w)$
136	127 135	anim12i	$⊢ ((B \in On \land w \in K \land K \in B) \land (z \subseteq f (K) \land f (K) \subseteq f (w))) \to (w \in B \land z \subseteq f (w))$
137		rabid	$⊢ w \in \{w \in B \| z \subseteq f (w)\} \leftrightarrow (w \in B \land z \subseteq f (w))$
138	136 137	sylibr	$⊢ ((B \in On \land w \in K \land K \in B) \land (z \subseteq f (K) \land f (K) \subseteq f (w))) \to w \in \{w \in B \| z \subseteq f (w)\}$
139		onnmin	$⊢ (\{w \in B \| z \subseteq f (w)\} \subseteq On \land w \in \{w \in B \| z \subseteq f (w)\}) \to \neg w \in ⋂ \{w \in B \| z \subseteq f (w)\}$
140	134 138 139	syl2anc	$⊢ ((B \in On \land w \in K \land K \in B) \land (z \subseteq f (K) \land f (K) \subseteq f (w))) \to \neg w \in ⋂ \{w \in B \| z \subseteq f (w)\}$
141	140	expr	$⊢ ((B \in On \land w \in K \land K \in B) \land z \subseteq f (K)) \to (f (K) \subseteq f (w) \to \neg w \in ⋂ \{w \in B \| z \subseteq f (w)\})$
142	125 117 123 132 141	syl31anc	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to (f (K) \subseteq f (w) \to \neg w \in ⋂ \{w \in B \| z \subseteq f (w)\})$
143	131 142	sylbird	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to (\neg f (w) \in f (K) \to \neg w \in ⋂ \{w \in B \| z \subseteq f (w)\})$
144	143	con4d	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to (w \in ⋂ \{w \in B \| z \subseteq f (w)\} \to f (w) \in f (K))$
145	118 144	syl5bi	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to (w \in K \to f (w) \in f (K))$
146	117 145	mpd	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \land w \in K) \to f (w) \in f (K)$
147	146	3expia	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K))) \to (w \in K \to f (w) \in f (K))$
148	147	ralrimiv	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K))) \to \forall w \in K f (w) \in f (K)$
149		fveq2	$⊢ y = K \to f (y) = f (K)$
150	149	eleq2d	$⊢ y = K \to (f (w) \in f (y) \leftrightarrow f (w) \in f (K))$
151	150	raleqbi1dv	$⊢ y = K \to (\forall w \in y f (w) \in f (y) \leftrightarrow \forall w \in K f (w) \in f (K))$
152	151 1	elrab2	$⊢ K \in C \leftrightarrow (K \in B \land \forall w \in K f (w) \in f (K))$
153	116 148 152	sylanbrc	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K))) \to K \in C$
154	153	expcom	$⊢ (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \to ((Ord A \land B \in On) \to K \in C)$
155	154	3expib	$⊢ f : B ⟶ A \to ((K \in B \land z \subseteq f (K)) \to ((Ord A \land B \in On) \to K \in C))$
156	155	com13	$⊢ (Ord A \land B \in On) \to ((K \in B \land z \subseteq f (K)) \to (f : B ⟶ A \to K \in C))$
157	115 156	syld	$⊢ (Ord A \land B \in On) \to (\exists w \in B z \subseteq f (w) \to (f : B ⟶ A \to K \in C))$
158	157	com23	$⊢ (Ord A \land B \in On) \to (f : B ⟶ A \to (\exists w \in B z \subseteq f (w) \to K \in C))$
159	158	imp31	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \to K \in C$
160		foelrn	$⊢ (O : dom O \underset{onto}{⟶} C \land K \in C) \to \exists v \in dom O K = O (v)$
161	17 159 160	syl2an2r	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \to \exists v \in dom O K = O (v)$
162		eleq1	$⊢ K = O (v) \to (K \in \{w \in B \| z \subseteq f (w)\} \leftrightarrow O (v) \in \{w \in B \| z \subseteq f (w)\})$
163	162	biimpcd	$⊢ K \in \{w \in B \| z \subseteq f (w)\} \to (K = O (v) \to O (v) \in \{w \in B \| z \subseteq f (w)\})$
164		fveq2	$⊢ x = O (v) \to f (x) = f (O (v))$
165	164	sseq2d	$⊢ x = O (v) \to (z \subseteq f (x) \leftrightarrow z \subseteq f (O (v)))$
166	67	sseq2d	$⊢ w = x \to (z \subseteq f (w) \leftrightarrow z \subseteq f (x))$
167	166	cbvrabv	$⊢ \{w \in B \| z \subseteq f (w)\} = \{x \in B \| z \subseteq f (x)\}$
168	165 167	elrab2	$⊢ O (v) \in \{w \in B \| z \subseteq f (w)\} \leftrightarrow (O (v) \in B \land z \subseteq f (O (v)))$
169	168	simprbi	$⊢ O (v) \in \{w \in B \| z \subseteq f (w)\} \to z \subseteq f (O (v))$
170	163 169	syl6	$⊢ K \in \{w \in B \| z \subseteq f (w)\} \to (K = O (v) \to z \subseteq f (O (v)))$
171	109 170	syl	$⊢ (B \in On \land \exists w \in B z \subseteq f (w)) \to (K = O (v) \to z \subseteq f (O (v)))$
172	171	ad5ant24	$⊢ ((((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \land v \in dom O) \to (K = O (v) \to z \subseteq f (O (v)))$
173	21	ad2antrr	$⊢ ((((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \land v \in dom O) \to O : dom O ⟶ B$
174		fvco3	$⊢ (O : dom O ⟶ B \land v \in dom O) \to (f \circ O) (v) = f (O (v))$
175	173 174	sylancom	$⊢ ((((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \land v \in dom O) \to (f \circ O) (v) = f (O (v))$
176	175	sseq2d	$⊢ ((((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \land v \in dom O) \to (z \subseteq (f \circ O) (v) \leftrightarrow z \subseteq f (O (v)))$
177	172 176	sylibrd	$⊢ ((((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \land v \in dom O) \to (K = O (v) \to z \subseteq (f \circ O) (v))$
178	177	reximdva	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \to (\exists v \in dom O K = O (v) \to \exists v \in dom O z \subseteq (f \circ O) (v))$
179	161 178	mpd	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \to \exists v \in dom O z \subseteq (f \circ O) (v)$
180	179	ex	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to (\exists w \in B z \subseteq f (w) \to \exists v \in dom O z \subseteq (f \circ O) (v))$
181	180	ralimdv	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to (\forall z \in A \exists w \in B z \subseteq f (w) \to \forall z \in A \exists v \in dom O z \subseteq (f \circ O) (v))$
182	181	impr	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to \forall z \in A \exists v \in dom O z \subseteq (f \circ O) (v)$
183	49 97 182	3jca	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to ((f \circ O) : dom O ⟶ A \land Smo (f \circ O) \land \forall z \in A \exists v \in dom O z \subseteq (f \circ O) (v))$
184		feq1	$⊢ g = f \circ O \to (g : dom O ⟶ A \leftrightarrow (f \circ O) : dom O ⟶ A)$
185		smoeq	$⊢ g = f \circ O \to (Smo g \leftrightarrow Smo (f \circ O))$
186		fveq1	$⊢ g = f \circ O \to g (v) = (f \circ O) (v)$
187	186	sseq2d	$⊢ g = f \circ O \to (z \subseteq g (v) \leftrightarrow z \subseteq (f \circ O) (v))$
188	187	rexbidv	$⊢ g = f \circ O \to (\exists v \in dom O z \subseteq g (v) \leftrightarrow \exists v \in dom O z \subseteq (f \circ O) (v))$
189	188	ralbidv	$⊢ g = f \circ O \to (\forall z \in A \exists v \in dom O z \subseteq g (v) \leftrightarrow \forall z \in A \exists v \in dom O z \subseteq (f \circ O) (v))$
190	184 185 189	3anbi123d	$⊢ g = f \circ O \to ((g : dom O ⟶ A \land Smo g \land \forall z \in A \exists v \in dom O z \subseteq g (v)) \leftrightarrow ((f \circ O) : dom O ⟶ A \land Smo (f \circ O) \land \forall z \in A \exists v \in dom O z \subseteq (f \circ O) (v)))$
191	45 183 190	spcedv	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to \exists g (g : dom O ⟶ A \land Smo g \land \forall z \in A \exists v \in dom O z \subseteq g (v))$
192		feq2	$⊢ x = dom O \to (g : x ⟶ A \leftrightarrow g : dom O ⟶ A)$
193		rexeq	$⊢ x = dom O \to (\exists v \in x z \subseteq g (v) \leftrightarrow \exists v \in dom O z \subseteq g (v))$
194	193	ralbidv	$⊢ x = dom O \to (\forall z \in A \exists v \in x z \subseteq g (v) \leftrightarrow \forall z \in A \exists v \in dom O z \subseteq g (v))$
195	192 194	3anbi13d	$⊢ x = dom O \to ((g : x ⟶ A \land Smo g \land \forall z \in A \exists v \in x z \subseteq g (v)) \leftrightarrow (g : dom O ⟶ A \land Smo g \land \forall z \in A \exists v \in dom O z \subseteq g (v)))$
196	195	exbidv	$⊢ x = dom O \to (\exists g (g : x ⟶ A \land Smo g \land \forall z \in A \exists v \in x z \subseteq g (v)) \leftrightarrow \exists g (g : dom O ⟶ A \land Smo g \land \forall z \in A \exists v \in dom O z \subseteq g (v)))$
197	196	rspcev	$⊢ (dom O \in suc B \land \exists g (g : dom O ⟶ A \land Smo g \land \forall z \in A \exists v \in dom O z \subseteq g (v))) \to \exists x \in suc B \exists g (g : x ⟶ A \land Smo g \land \forall z \in A \exists v \in x z \subseteq g (v))$
198	39 191 197	syl2anc	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w))) \to \exists x \in suc B \exists g (g : x ⟶ A \land Smo g \land \forall z \in A \exists v \in x z \subseteq g (v))$
199	198	ex	$⊢ (Ord A \land B \in On) \to ((f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w)) \to \exists x \in suc B \exists g (g : x ⟶ A \land Smo g \land \forall z \in A \exists v \in x z \subseteq g (v)))$
200	199	exlimdv	$⊢ (Ord A \land B \in On) \to (\exists f (f : B ⟶ A \land \forall z \in A \exists w \in B z \subseteq f (w)) \to \exists x \in suc B \exists g (g : x ⟶ A \land Smo g \land \forall z \in A \exists v \in x z \subseteq g (v)))$

Metamath Proof Explorer

Theorem cofsmo

Proof