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	46 47	fcod	$⊢ ((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$
49		simpr	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to f : B ⟶ A$
50	49 21	fcod	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to (f \circ O) : dom O ⟶ A$
51		ordsson	$⊢ Ord A \to A \subseteq On$
52	51	ad2antrr	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to A \subseteq On$
53	24 26	syl	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to Ord dom O$
54	17 18	syl	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to O : dom O ⟶ C$
55		simpl	$⊢ (s \in dom O \land t \in s) \to s \in dom O$
56		ffvelrn	$⊢ (O : dom O ⟶ C \land s \in dom O) \to O (s) \in C$
57	54 55 56	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$
58		ffn	$⊢ O : dom O ⟶ C \to O Fn dom O$
59	17 18 58	3syl	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to O Fn dom O$
60	59 31	jca	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to (O Fn dom O \land Smo O)$
61		smoel2	$⊢ ((O Fn dom O \land Smo O) \land (s \in dom O \land t \in s)) \to O (t) \in O (s)$
62	60 61	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)$
63		fveq2	$⊢ z = O (s) \to f (z) = f (O (s))$
64	63	eleq2d	$⊢ z = O (s) \to (f (x) \in f (z) \leftrightarrow f (x) \in f (O (s)))$
65	64	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)))$
66		fveq2	$⊢ w = x \to f (w) = f (x)$
67	66	eleq1d	$⊢ w = x \to (f (w) \in f (y) \leftrightarrow f (x) \in f (y))$
68	67	cbvralvw	$⊢ \forall w \in y f (w) \in f (y) \leftrightarrow \forall x \in y f (x) \in f (y)$
69		fveq2	$⊢ y = z \to f (y) = f (z)$
70	69	eleq2d	$⊢ y = z \to (f (x) \in f (y) \leftrightarrow f (x) \in f (z))$
71	70	raleqbi1dv	$⊢ y = z \to (\forall x \in y f (x) \in f (y) \leftrightarrow \forall x \in z f (x) \in f (z))$
72	68 71	syl5bb	$⊢ y = z \to (\forall w \in y f (w) \in f (y) \leftrightarrow \forall x \in z f (x) \in f (z))$
73	72	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)\}$
74	1 73	eqtri	$⊢ C = \{z \in B \| \forall x \in z f (x) \in f (z)\}$
75	65 74	elrab2	$⊢ O (s) \in C \leftrightarrow (O (s) \in B \land \forall x \in O (s) f (x) \in f (O (s)))$
76	75	simprbi	$⊢ O (s) \in C \to \forall x \in O (s) f (x) \in f (O (s))$
77		fveq2	$⊢ x = O (t) \to f (x) = f (O (t))$
78	77	eleq1d	$⊢ x = O (t) \to (f (x) \in f (O (s)) \leftrightarrow f (O (t)) \in f (O (s)))$
79	78	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)))$
80	76 79	syl	$⊢ O (s) \in C \to (O (t) \in O (s) \to f (O (t)) \in f (O (s)))$
81	57 62 80	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))$
82		ordtr1	$⊢ Ord dom O \to ((t \in s \land s \in dom O) \to t \in dom O)$
83	82	ancomsd	$⊢ Ord dom O \to ((s \in dom O \land t \in s) \to t \in dom O)$
84	24 26 83	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)$
85	84	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$
86		fvco3	$⊢ (O : dom O ⟶ B \land t \in dom O) \to (f \circ O) (t) = f (O (t))$
87	21 85 86	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))$
88		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$
89		fvco3	$⊢ (O : dom O ⟶ B \land s \in dom O) \to (f \circ O) (s) = f (O (s))$
90	21 88 89	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))$
91	81 87 90	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)$
92	91	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)$
93		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))$
94	93	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)$
95	50 52 53 92 94	syl13anc	$⊢ ((Ord A \land B \in On) \land f : B ⟶ A) \to Smo (f \circ O)$
96	95	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)$
97		rabn0	$⊢ \{w \in B \| z \subseteq f (w)\} \neq \emptyset \leftrightarrow \exists w \in B z \subseteq f (w)$
98		ssrab2	$⊢ \{w \in B \| z \subseteq f (w)\} \subseteq B$
99	98 7	sstrid	$⊢ B \in On \to \{w \in B \| z \subseteq f (w)\} \subseteq On$
100		fveq2	$⊢ x = w \to f (x) = f (w)$
101	100	sseq2d	$⊢ x = w \to (z \subseteq f (x) \leftrightarrow z \subseteq f (w))$
102	101	cbvrabv	$⊢ \{x \in B \| z \subseteq f (x)\} = \{w \in B \| z \subseteq f (w)\}$
103	102	inteqi	$⊢ ⋂ \{x \in B \| z \subseteq f (x)\} = ⋂ \{w \in B \| z \subseteq f (w)\}$
104	2 103	eqtri	$⊢ K = ⋂ \{w \in B \| z \subseteq f (w)\}$
105		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)\}$
106	104 105	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)\}$
107	99 106	sylan	$⊢ (B \in On \land \{w \in B \| z \subseteq f (w)\} \neq \emptyset) \to K \in \{w \in B \| z \subseteq f (w)\}$
108	97 107	sylan2br	$⊢ (B \in On \land \exists w \in B z \subseteq f (w)) \to K \in \{w \in B \| z \subseteq f (w)\}$
109		fveq2	$⊢ w = K \to f (w) = f (K)$
110	109	sseq2d	$⊢ w = K \to (z \subseteq f (w) \leftrightarrow z \subseteq f (K))$
111	110	elrab	$⊢ K \in \{w \in B \| z \subseteq f (w)\} \leftrightarrow (K \in B \land z \subseteq f (K))$
112	108 111	sylib	$⊢ (B \in On \land \exists w \in B z \subseteq f (w)) \to (K \in B \land z \subseteq f (K))$
113	112	ex	$⊢ B \in On \to (\exists w \in B z \subseteq f (w) \to (K \in B \land z \subseteq f (K)))$
114	113	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)))$
115		simpr2	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K))) \to K \in B$
116		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$
117	104	eleq2i	$⊢ w \in K \leftrightarrow w \in ⋂ \{w \in B \| z \subseteq f (w)\}$
118		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$
119		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$
120	119 51	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$
121	118 120	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$
122		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$
123	121 122	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$
124		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$
125		ontr1	$⊢ B \in On \to ((w \in K \land K \in B) \to w \in B)$
126	125	3impib	$⊢ (B \in On \land w \in K \land K \in B) \to w \in B$
127	124 116 122 126	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$
128	121 127	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$
129		ontri1	$⊢ (f (K) \in On \land f (w) \in On) \to (f (K) \subseteq f (w) \leftrightarrow \neg f (w) \in f (K))$
130	123 128 129	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))$
131		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)$
132		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$
133	132 99	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$
134		sstr	$⊢ (z \subseteq f (K) \land f (K) \subseteq f (w)) \to z \subseteq f (w)$
135	126 134	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))$
136		rabid	$⊢ w \in \{w \in B \| z \subseteq f (w)\} \leftrightarrow (w \in B \land z \subseteq f (w))$
137	135 136	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)\}$
138		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)\}$
139	133 137 138	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)\}$
140	139	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)\})$
141	124 116 122 131 140	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)\})$
142	130 141	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)\})$
143	142	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))$
144	117 143	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))$
145	116 144	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)$
146	145	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))$
147	146	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)$
148		fveq2	$⊢ y = K \to f (y) = f (K)$
149	148	eleq2d	$⊢ y = K \to (f (w) \in f (y) \leftrightarrow f (w) \in f (K))$
150	149	raleqbi1dv	$⊢ y = K \to (\forall w \in y f (w) \in f (y) \leftrightarrow \forall w \in K f (w) \in f (K))$
151	150 1	elrab2	$⊢ K \in C \leftrightarrow (K \in B \land \forall w \in K f (w) \in f (K))$
152	115 147 151	sylanbrc	$⊢ ((Ord A \land B \in On) \land (f : B ⟶ A \land K \in B \land z \subseteq f (K))) \to K \in C$
153	152	expcom	$⊢ (f : B ⟶ A \land K \in B \land z \subseteq f (K)) \to ((Ord A \land B \in On) \to K \in C)$
154	153	3expib	$⊢ f : B ⟶ A \to ((K \in B \land z \subseteq f (K)) \to ((Ord A \land B \in On) \to K \in C))$
155	154	com13	$⊢ (Ord A \land B \in On) \to ((K \in B \land z \subseteq f (K)) \to (f : B ⟶ A \to K \in C))$
156	114 155	syld	$⊢ (Ord A \land B \in On) \to (\exists w \in B z \subseteq f (w) \to (f : B ⟶ A \to K \in C))$
157	156	com23	$⊢ (Ord A \land B \in On) \to (f : B ⟶ A \to (\exists w \in B z \subseteq f (w) \to K \in C))$
158	157	imp31	$⊢ (((Ord A \land B \in On) \land f : B ⟶ A) \land \exists w \in B z \subseteq f (w)) \to K \in C$
159		foelrn	$⊢ (O : dom O \underset{onto}{⟶} C \land K \in C) \to \exists v \in dom O K = O (v)$
160	17 158 159	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)$
161		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)\})$
162	161	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)\})$
163		fveq2	$⊢ x = O (v) \to f (x) = f (O (v))$
164	163	sseq2d	$⊢ x = O (v) \to (z \subseteq f (x) \leftrightarrow z \subseteq f (O (v)))$
165	66	sseq2d	$⊢ w = x \to (z \subseteq f (w) \leftrightarrow z \subseteq f (x))$
166	165	cbvrabv	$⊢ \{w \in B \| z \subseteq f (w)\} = \{x \in B \| z \subseteq f (x)\}$
167	164 166	elrab2	$⊢ O (v) \in \{w \in B \| z \subseteq f (w)\} \leftrightarrow (O (v) \in B \land z \subseteq f (O (v)))$
168	167	simprbi	$⊢ O (v) \in \{w \in B \| z \subseteq f (w)\} \to z \subseteq f (O (v))$
169	162 168	syl6	$⊢ K \in \{w \in B \| z \subseteq f (w)\} \to (K = O (v) \to z \subseteq f (O (v)))$
170	108 169	syl	$⊢ (B \in On \land \exists w \in B z \subseteq f (w)) \to (K = O (v) \to z \subseteq f (O (v)))$
171	170	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)))$
172	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$
173		fvco3	$⊢ (O : dom O ⟶ B \land v \in dom O) \to (f \circ O) (v) = f (O (v))$
174	172 173	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))$
175	174	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)))$
176	171 175	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))$
177	176	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))$
178	160 177	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)$
179	178	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))$
180	179	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))$
181	180	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)$
182	48 96 181	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))$
183		feq1	$⊢ g = f \circ O \to (g : dom O ⟶ A \leftrightarrow (f \circ O) : dom O ⟶ A)$
184		smoeq	$⊢ g = f \circ O \to (Smo g \leftrightarrow Smo (f \circ O))$
185		fveq1	$⊢ g = f \circ O \to g (v) = (f \circ O) (v)$
186	185	sseq2d	$⊢ g = f \circ O \to (z \subseteq g (v) \leftrightarrow z \subseteq (f \circ O) (v))$
187	186	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))$
188	187	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))$
189	183 184 188	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)))$
190	45 182 189	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))$
191		feq2	$⊢ x = dom O \to (g : x ⟶ A \leftrightarrow g : dom O ⟶ A)$
192		rexeq	$⊢ x = dom O \to (\exists v \in x z \subseteq g (v) \leftrightarrow \exists v \in dom O z \subseteq g (v))$
193	192	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))$
194	191 193	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)))$
195	194	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)))$
196	195	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))$
197	39 190 196	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))$
198	197	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)))$
199	198	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