Theorem oawordeulem

Description: Lemma for oawordex . (Contributed by NM, 11-Dec-2004)

	Ref	Expression
Hypotheses	oawordeulem.1	$$⊢A\in \mathrm{On}$$
	oawordeulem.2	$$⊢B\in \mathrm{On}$$
	oawordeulem.3	$$⊢S=\left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
Assertion	oawordeulem	$$⊢A\subseteq B\to \exists !x\in \mathrm{On}A{+}_{𝑜}x=B$$

Proof

Step	Hyp	Ref	Expression
1		oawordeulem.1	$$⊢A\in \mathrm{On}$$
2		oawordeulem.2	$$⊢B\in \mathrm{On}$$
3		oawordeulem.3	$$⊢S=\left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
4	3	ssrab3	$$⊢S\subseteq \mathrm{On}$$
5		oaword2	$$⊢\left(B\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to B\subseteq A{+}_{𝑜}B$$
6	2 1 5	mp2an	$$⊢B\subseteq A{+}_{𝑜}B$$
7		oveq2	$$⊢y=B\to A{+}_{𝑜}y=A{+}_{𝑜}B$$
8	7	sseq2d	$$⊢y=B\to \left(B\subseteq A{+}_{𝑜}y\leftrightarrow B\subseteq A{+}_{𝑜}B\right)$$
9	8 3	elrab2	$$⊢B\in S\leftrightarrow \left(B\in \mathrm{On}\wedge B\subseteq A{+}_{𝑜}B\right)$$
10	2 6 9	mpbir2an	$$⊢B\in S$$
11	10	ne0ii	$$⊢S\ne \varnothing$$
12		oninton	$$⊢\left(S\subseteq \mathrm{On}\wedge S\ne \varnothing \right)\to \bigcap S\in \mathrm{On}$$
13	4 11 12	mp2an	$$⊢\bigcap S\in \mathrm{On}$$
14		onzsl	$$⊢\bigcap S\in \mathrm{On}\leftrightarrow \left(\bigcap S=\varnothing \vee \exists z\in \mathrm{On}\bigcap S=\mathrm{suc}z\vee \left(\bigcap S\in \mathrm{V}\wedge \mathrm{Lim}\bigcap S\right)\right)$$
15	13 14	mpbi	$$⊢\left(\bigcap S=\varnothing \vee \exists z\in \mathrm{On}\bigcap S=\mathrm{suc}z\vee \left(\bigcap S\in \mathrm{V}\wedge \mathrm{Lim}\bigcap S\right)\right)$$
16		oveq2	$$⊢\bigcap S=\varnothing \to A{+}_{𝑜}\bigcap S=A{+}_{𝑜}\varnothing$$
17		oa0	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =A$$
18	1 17	ax-mp	$$⊢A{+}_{𝑜}\varnothing =A$$
19	16 18	eqtrdi	$$⊢\bigcap S=\varnothing \to A{+}_{𝑜}\bigcap S=A$$
20	19	sseq1d	$$⊢\bigcap S=\varnothing \to \left(A{+}_{𝑜}\bigcap S\subseteq B\leftrightarrow A\subseteq B\right)$$
21	20	biimprd	$$⊢\bigcap S=\varnothing \to \left(A\subseteq B\to A{+}_{𝑜}\bigcap S\subseteq B\right)$$
22		oveq2	$$⊢\bigcap S=\mathrm{suc}z\to A{+}_{𝑜}\bigcap S=A{+}_{𝑜}\mathrm{suc}z$$
23		oasuc	$$⊢\left(A\in \mathrm{On}\wedge z\in \mathrm{On}\right)\to A{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(A{+}_{𝑜}z\right)$$
24	1 23	mpan	$$⊢z\in \mathrm{On}\to A{+}_{𝑜}\mathrm{suc}z=\mathrm{suc}\left(A{+}_{𝑜}z\right)$$
25	22 24	sylan9eqr	$$⊢\left(z\in \mathrm{On}\wedge \bigcap S=\mathrm{suc}z\right)\to A{+}_{𝑜}\bigcap S=\mathrm{suc}\left(A{+}_{𝑜}z\right)$$
26		vex	$$⊢z\in \mathrm{V}$$
27	26	sucid	$$⊢z\in \mathrm{suc}z$$
28		eleq2	$$⊢\bigcap S=\mathrm{suc}z\to \left(z\in \bigcap S\leftrightarrow z\in \mathrm{suc}z\right)$$
29	27 28	mpbiri	$$⊢\bigcap S=\mathrm{suc}z\to z\in \bigcap S$$
30	13	oneli	$$⊢z\in \bigcap S\to z\in \mathrm{On}$$
31	3	inteqi	$$⊢\bigcap S=\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
32	31	eleq2i	$$⊢z\in \bigcap S\leftrightarrow z\in \bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
33		oveq2	$$⊢y=z\to A{+}_{𝑜}y=A{+}_{𝑜}z$$
34	33	sseq2d	$$⊢y=z\to \left(B\subseteq A{+}_{𝑜}y\leftrightarrow B\subseteq A{+}_{𝑜}z\right)$$
35	34	onnminsb	$$⊢z\in \mathrm{On}\to \left(z\in \bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}\to \neg B\subseteq A{+}_{𝑜}z\right)$$
36	32 35	syl5bi	$$⊢z\in \mathrm{On}\to \left(z\in \bigcap S\to \neg B\subseteq A{+}_{𝑜}z\right)$$
37		oacl	$$⊢\left(A\in \mathrm{On}\wedge z\in \mathrm{On}\right)\to A{+}_{𝑜}z\in \mathrm{On}$$
38	1 37	mpan	$$⊢z\in \mathrm{On}\to A{+}_{𝑜}z\in \mathrm{On}$$
39		ontri1	$$⊢\left(B\in \mathrm{On}\wedge A{+}_{𝑜}z\in \mathrm{On}\right)\to \left(B\subseteq A{+}_{𝑜}z\leftrightarrow \neg A{+}_{𝑜}z\in B\right)$$
40	2 38 39	sylancr	$$⊢z\in \mathrm{On}\to \left(B\subseteq A{+}_{𝑜}z\leftrightarrow \neg A{+}_{𝑜}z\in B\right)$$
41	40	con2bid	$$⊢z\in \mathrm{On}\to \left(A{+}_{𝑜}z\in B\leftrightarrow \neg B\subseteq A{+}_{𝑜}z\right)$$
42	36 41	sylibrd	$$⊢z\in \mathrm{On}\to \left(z\in \bigcap S\to A{+}_{𝑜}z\in B\right)$$
43	30 42	mpcom	$$⊢z\in \bigcap S\to A{+}_{𝑜}z\in B$$
44	2	onordi	$$⊢\mathrm{Ord}B$$
45		ordsucss	$$⊢\mathrm{Ord}B\to \left(A{+}_{𝑜}z\in B\to \mathrm{suc}\left(A{+}_{𝑜}z\right)\subseteq B\right)$$
46	44 45	ax-mp	$$⊢A{+}_{𝑜}z\in B\to \mathrm{suc}\left(A{+}_{𝑜}z\right)\subseteq B$$
47	29 43 46	3syl	$$⊢\bigcap S=\mathrm{suc}z\to \mathrm{suc}\left(A{+}_{𝑜}z\right)\subseteq B$$
48	47	adantl	$$⊢\left(z\in \mathrm{On}\wedge \bigcap S=\mathrm{suc}z\right)\to \mathrm{suc}\left(A{+}_{𝑜}z\right)\subseteq B$$
49	25 48	eqsstrd	$$⊢\left(z\in \mathrm{On}\wedge \bigcap S=\mathrm{suc}z\right)\to A{+}_{𝑜}\bigcap S\subseteq B$$
50	49	rexlimiva	$$⊢\exists z\in \mathrm{On}\bigcap S=\mathrm{suc}z\to A{+}_{𝑜}\bigcap S\subseteq B$$
51	50	a1d	$$⊢\exists z\in \mathrm{On}\bigcap S=\mathrm{suc}z\to \left(A\subseteq B\to A{+}_{𝑜}\bigcap S\subseteq B\right)$$
52		oalim	$$⊢\left(A\in \mathrm{On}\wedge \left(\bigcap S\in \mathrm{V}\wedge \mathrm{Lim}\bigcap S\right)\right)\to A{+}_{𝑜}\bigcap S=\bigcup _{z\in \bigcap S}\left(A{+}_{𝑜}z\right)$$
53	1 52	mpan	$$⊢\left(\bigcap S\in \mathrm{V}\wedge \mathrm{Lim}\bigcap S\right)\to A{+}_{𝑜}\bigcap S=\bigcup _{z\in \bigcap S}\left(A{+}_{𝑜}z\right)$$
54		iunss	$$⊢\bigcup _{z\in \bigcap S}\left(A{+}_{𝑜}z\right)\subseteq B\leftrightarrow \forall z\in \bigcap SA{+}_{𝑜}z\subseteq B$$
55	2	onelssi	$$⊢A{+}_{𝑜}z\in B\to A{+}_{𝑜}z\subseteq B$$
56	43 55	syl	$$⊢z\in \bigcap S\to A{+}_{𝑜}z\subseteq B$$
57	54 56	mprgbir	$$⊢\bigcup _{z\in \bigcap S}\left(A{+}_{𝑜}z\right)\subseteq B$$
58	53 57	eqsstrdi	$$⊢\left(\bigcap S\in \mathrm{V}\wedge \mathrm{Lim}\bigcap S\right)\to A{+}_{𝑜}\bigcap S\subseteq B$$
59	58	a1d	$$⊢\left(\bigcap S\in \mathrm{V}\wedge \mathrm{Lim}\bigcap S\right)\to \left(A\subseteq B\to A{+}_{𝑜}\bigcap S\subseteq B\right)$$
60	21 51 59	3jaoi	$$⊢\left(\bigcap S=\varnothing \vee \exists z\in \mathrm{On}\bigcap S=\mathrm{suc}z\vee \left(\bigcap S\in \mathrm{V}\wedge \mathrm{Lim}\bigcap S\right)\right)\to \left(A\subseteq B\to A{+}_{𝑜}\bigcap S\subseteq B\right)$$
61	15 60	ax-mp	$$⊢A\subseteq B\to A{+}_{𝑜}\bigcap S\subseteq B$$
62	8	rspcev	$$⊢\left(B\in \mathrm{On}\wedge B\subseteq A{+}_{𝑜}B\right)\to \exists y\in \mathrm{On}B\subseteq A{+}_{𝑜}y$$
63	2 6 62	mp2an	$$⊢\exists y\in \mathrm{On}B\subseteq A{+}_{𝑜}y$$
64		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
65		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
66		nfcv	$$⊢\underset{\_}{Ⅎ}y{+}_{𝑜}$$
67		nfrab1	$$⊢\underset{\_}{Ⅎ}y\left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
68	67	nfint	$$⊢\underset{\_}{Ⅎ}y\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
69	65 66 68	nfov	$$⊢\underset{\_}{Ⅎ}y\left(A{+}_{𝑜}\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}\right)$$
70	64 69	nfss	$$⊢ℲyB\subseteq A{+}_{𝑜}\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
71		oveq2	$$⊢y=\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}\to A{+}_{𝑜}y=A{+}_{𝑜}\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
72	71	sseq2d	$$⊢y=\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}\to \left(B\subseteq A{+}_{𝑜}y\leftrightarrow B\subseteq A{+}_{𝑜}\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}\right)$$
73	70 72	onminsb	$$⊢\exists y\in \mathrm{On}B\subseteq A{+}_{𝑜}y\to B\subseteq A{+}_{𝑜}\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
74	63 73	ax-mp	$$⊢B\subseteq A{+}_{𝑜}\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
75	31	oveq2i	$$⊢A{+}_{𝑜}\bigcap S=A{+}_{𝑜}\bigcap \left\{y\in \mathrm{On}|B\subseteq A{+}_{𝑜}y\right\}$$
76	74 75	sseqtrri	$$⊢B\subseteq A{+}_{𝑜}\bigcap S$$
77		eqss	$$⊢A{+}_{𝑜}\bigcap S=B\leftrightarrow \left(A{+}_{𝑜}\bigcap S\subseteq B\wedge B\subseteq A{+}_{𝑜}\bigcap S\right)$$
78	61 76 77	sylanblrc	$$⊢A\subseteq B\to A{+}_{𝑜}\bigcap S=B$$
79		oveq2	$$⊢x=\bigcap S\to A{+}_{𝑜}x=A{+}_{𝑜}\bigcap S$$
80	79	eqeq1d	$$⊢x=\bigcap S\to \left(A{+}_{𝑜}x=B\leftrightarrow A{+}_{𝑜}\bigcap S=B\right)$$
81	80	rspcev	$$⊢\left(\bigcap S\in \mathrm{On}\wedge A{+}_{𝑜}\bigcap S=B\right)\to \exists x\in \mathrm{On}A{+}_{𝑜}x=B$$
82	13 78 81	sylancr	$$⊢A\subseteq B\to \exists x\in \mathrm{On}A{+}_{𝑜}x=B$$
83		eqtr3	$$⊢\left(A{+}_{𝑜}x=B\wedge A{+}_{𝑜}y=B\right)\to A{+}_{𝑜}x=A{+}_{𝑜}y$$
84		oacan	$$⊢\left(A\in \mathrm{On}\wedge x\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to \left(A{+}_{𝑜}x=A{+}_{𝑜}y\leftrightarrow x=y\right)$$
85	1 84	mp3an1	$$⊢\left(x\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to \left(A{+}_{𝑜}x=A{+}_{𝑜}y\leftrightarrow x=y\right)$$
86	83 85	syl5ib	$$⊢\left(x\in \mathrm{On}\wedge y\in \mathrm{On}\right)\to \left(\left(A{+}_{𝑜}x=B\wedge A{+}_{𝑜}y=B\right)\to x=y\right)$$
87	86	rgen2	$$⊢\forall x\in \mathrm{On}\forall y\in \mathrm{On}\left(\left(A{+}_{𝑜}x=B\wedge A{+}_{𝑜}y=B\right)\to x=y\right)$$
88		oveq2	$$⊢x=y\to A{+}_{𝑜}x=A{+}_{𝑜}y$$
89	88	eqeq1d	$$⊢x=y\to \left(A{+}_{𝑜}x=B\leftrightarrow A{+}_{𝑜}y=B\right)$$
90	89	reu4	$$⊢\exists !x\in \mathrm{On}A{+}_{𝑜}x=B\leftrightarrow \left(\exists x\in \mathrm{On}A{+}_{𝑜}x=B\wedge \forall x\in \mathrm{On}\forall y\in \mathrm{On}\left(\left(A{+}_{𝑜}x=B\wedge A{+}_{𝑜}y=B\right)\to x=y\right)\right)$$
91	82 87 90	sylanblrc	$$⊢A\subseteq B\to \exists !x\in \mathrm{On}A{+}_{𝑜}x=B$$