Theorem wdom2d

Description: Deduce weak dominance from an implicit onto function (stated in a way which avoids ax-rep ). (Contributed by Stefan O'Rear, 13-Feb-2015)

	Ref	Expression
Hypotheses	wdom2d.a	$$⊢\phi \to A\in V$$
	wdom2d.b	$$⊢\phi \to B\in W$$
	wdom2d.o	$$⊢\left(\phi \wedge x\in A\right)\to \exists y\in Bx=X$$
Assertion	wdom2d	$$⊢\phi \to A{\preccurlyeq }^{*}B$$

Proof

Step	Hyp	Ref	Expression
1		wdom2d.a	$$⊢\phi \to A\in V$$
2		wdom2d.b	$$⊢\phi \to B\in W$$
3		wdom2d.o	$$⊢\left(\phi \wedge x\in A\right)\to \exists y\in Bx=X$$
4		rabexg	$$⊢B\in W\to \left\{z\in B|⦋z/y⦌X\in A\right\}\in \mathrm{V}$$
5	2 4	syl	$$⊢\phi \to \left\{z\in B|⦋z/y⦌X\in A\right\}\in \mathrm{V}$$
6	5 1	xpexd	$$⊢\phi \to \left\{z\in B|⦋z/y⦌X\in A\right\}\times A\in \mathrm{V}$$
7		csbeq1	$$⊢z=w\to ⦋z/y⦌X=⦋w/y⦌X$$
8	7	eleq1d	$$⊢z=w\to \left(⦋z/y⦌X\in A\leftrightarrow ⦋w/y⦌X\in A\right)$$
9	8	elrab	$$⊢w\in \left\{z\in B|⦋z/y⦌X\in A\right\}\leftrightarrow \left(w\in B\wedge ⦋w/y⦌X\in A\right)$$
10	9	simprbi	$$⊢w\in \left\{z\in B|⦋z/y⦌X\in A\right\}\to ⦋w/y⦌X\in A$$
11	10	adantl	$$⊢\left(\phi \wedge w\in \left\{z\in B|⦋z/y⦌X\in A\right\}\right)\to ⦋w/y⦌X\in A$$
12	11	fmpttd	$$⊢\phi \to \left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right):\left\{z\in B|⦋z/y⦌X\in A\right\}⟶A$$
13		fssxp	$$⊢\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right):\left\{z\in B|⦋z/y⦌X\in A\right\}⟶A\to \left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\subseteq \left\{z\in B|⦋z/y⦌X\in A\right\}\times A$$
14	12 13	syl	$$⊢\phi \to \left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\subseteq \left\{z\in B|⦋z/y⦌X\in A\right\}\times A$$
15	6 14	ssexd	$$⊢\phi \to \left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\in \mathrm{V}$$
16		eleq1	$$⊢x=X\to \left(x\in A\leftrightarrow X\in A\right)$$
17	16	biimpcd	$$⊢x\in A\to \left(x=X\to X\in A\right)$$
18	17	ancrd	$$⊢x\in A\to \left(x=X\to \left(X\in A\wedge x=X\right)\right)$$
19	18	adantl	$$⊢\left(\phi \wedge x\in A\right)\to \left(x=X\to \left(X\in A\wedge x=X\right)\right)$$
20	19	reximdv	$$⊢\left(\phi \wedge x\in A\right)\to \left(\exists y\in Bx=X\to \exists y\in B\left(X\in A\wedge x=X\right)\right)$$
21	3 20	mpd	$$⊢\left(\phi \wedge x\in A\right)\to \exists y\in B\left(X\in A\wedge x=X\right)$$
22		nfv	$$⊢Ⅎv\left(X\in A\wedge x=X\right)$$
23		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋v/y⦌X$$
24	23	nfel1	$$⊢Ⅎy⦋v/y⦌X\in A$$
25	23	nfeq2	$$⊢Ⅎyx=⦋v/y⦌X$$
26	24 25	nfan	$$⊢Ⅎy\left(⦋v/y⦌X\in A\wedge x=⦋v/y⦌X\right)$$
27		csbeq1a	$$⊢y=v\to X=⦋v/y⦌X$$
28	27	eleq1d	$$⊢y=v\to \left(X\in A\leftrightarrow ⦋v/y⦌X\in A\right)$$
29	27	eqeq2d	$$⊢y=v\to \left(x=X\leftrightarrow x=⦋v/y⦌X\right)$$
30	28 29	anbi12d	$$⊢y=v\to \left(\left(X\in A\wedge x=X\right)\leftrightarrow \left(⦋v/y⦌X\in A\wedge x=⦋v/y⦌X\right)\right)$$
31	22 26 30	cbvrexw	$$⊢\exists y\in B\left(X\in A\wedge x=X\right)\leftrightarrow \exists v\in B\left(⦋v/y⦌X\in A\wedge x=⦋v/y⦌X\right)$$
32	21 31	sylib	$$⊢\left(\phi \wedge x\in A\right)\to \exists v\in B\left(⦋v/y⦌X\in A\wedge x=⦋v/y⦌X\right)$$
33		csbeq1	$$⊢z=v\to ⦋z/y⦌X=⦋v/y⦌X$$
34	33	eleq1d	$$⊢z=v\to \left(⦋z/y⦌X\in A\leftrightarrow ⦋v/y⦌X\in A\right)$$
35	34	elrab	$$⊢v\in \left\{z\in B|⦋z/y⦌X\in A\right\}\leftrightarrow \left(v\in B\wedge ⦋v/y⦌X\in A\right)$$
36	35	simprbi	$$⊢v\in \left\{z\in B|⦋z/y⦌X\in A\right\}\to ⦋v/y⦌X\in A$$
37		csbeq1	$$⊢w=v\to ⦋w/y⦌X=⦋v/y⦌X$$
38		eqid	$$⊢\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)=\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)$$
39	37 38	fvmptg	$$⊢\left(v\in \left\{z\in B|⦋z/y⦌X\in A\right\}\wedge ⦋v/y⦌X\in A\right)\to \left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\left(v\right)=⦋v/y⦌X$$
40	36 39	mpdan	$$⊢v\in \left\{z\in B|⦋z/y⦌X\in A\right\}\to \left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\left(v\right)=⦋v/y⦌X$$
41	40	eqeq2d	$$⊢v\in \left\{z\in B|⦋z/y⦌X\in A\right\}\to \left(x=\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\left(v\right)\leftrightarrow x=⦋v/y⦌X\right)$$
42	41	rexbiia	$$⊢\exists v\in \left\{z\in B|⦋z/y⦌X\in A\right\}x=\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\left(v\right)\leftrightarrow \exists v\in \left\{z\in B|⦋z/y⦌X\in A\right\}x=⦋v/y⦌X$$
43	34	rexrab	$$⊢\exists v\in \left\{z\in B|⦋z/y⦌X\in A\right\}x=⦋v/y⦌X\leftrightarrow \exists v\in B\left(⦋v/y⦌X\in A\wedge x=⦋v/y⦌X\right)$$
44	42 43	bitri	$$⊢\exists v\in \left\{z\in B|⦋z/y⦌X\in A\right\}x=\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\left(v\right)\leftrightarrow \exists v\in B\left(⦋v/y⦌X\in A\wedge x=⦋v/y⦌X\right)$$
45	32 44	sylibr	$$⊢\left(\phi \wedge x\in A\right)\to \exists v\in \left\{z\in B|⦋z/y⦌X\in A\right\}x=\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\left(v\right)$$
46	45	ralrimiva	$$⊢\phi \to \forall x\in A\exists v\in \left\{z\in B|⦋z/y⦌X\in A\right\}x=\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\left(v\right)$$
47		dffo3	$$⊢\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right):\left\{z\in B|⦋z/y⦌X\in A\right\}\underset{onto}{⟶}A\leftrightarrow \left(\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right):\left\{z\in B|⦋z/y⦌X\in A\right\}⟶A\wedge \forall x\in A\exists v\in \left\{z\in B|⦋z/y⦌X\in A\right\}x=\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\left(v\right)\right)$$
48	12 46 47	sylanbrc	$$⊢\phi \to \left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right):\left\{z\in B|⦋z/y⦌X\in A\right\}\underset{onto}{⟶}A$$
49		fowdom	$$⊢\left(\left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right)\in \mathrm{V}\wedge \left(w\in \left\{z\in B|⦋z/y⦌X\in A\right\}⟼⦋w/y⦌X\right):\left\{z\in B|⦋z/y⦌X\in A\right\}\underset{onto}{⟶}A\right)\to A{\preccurlyeq }^{*}\left\{z\in B|⦋z/y⦌X\in A\right\}$$
50	15 48 49	syl2anc	$$⊢\phi \to A{\preccurlyeq }^{*}\left\{z\in B|⦋z/y⦌X\in A\right\}$$
51		ssrab2	$$⊢\left\{z\in B|⦋z/y⦌X\in A\right\}\subseteq B$$
52		ssdomg	$$⊢B\in W\to \left(\left\{z\in B|⦋z/y⦌X\in A\right\}\subseteq B\to \left\{z\in B|⦋z/y⦌X\in A\right\}\preccurlyeq B\right)$$
53	51 52	mpi	$$⊢B\in W\to \left\{z\in B|⦋z/y⦌X\in A\right\}\preccurlyeq B$$
54		domwdom	$$⊢\left\{z\in B|⦋z/y⦌X\in A\right\}\preccurlyeq B\to \left\{z\in B|⦋z/y⦌X\in A\right\}{\preccurlyeq }^{*}B$$
55	2 53 54	3syl	$$⊢\phi \to \left\{z\in B|⦋z/y⦌X\in A\right\}{\preccurlyeq }^{*}B$$
56		wdomtr	$$⊢\left(A{\preccurlyeq }^{*}\left\{z\in B|⦋z/y⦌X\in A\right\}\wedge \left\{z\in B|⦋z/y⦌X\in A\right\}{\preccurlyeq }^{*}B\right)\to A{\preccurlyeq }^{*}B$$
57	50 55 56	syl2anc	$$⊢\phi \to A{\preccurlyeq }^{*}B$$