Theorem wdom2d2

Description: Deduction for weak dominance by a Cartesian product.MOVABLE (Contributed by Stefan O'Rear, 10-Jul-2015)

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

Proof

Step	Hyp	Ref	Expression
1		wdom2d2.a	$$⊢\phi \to A\in V$$
2		wdom2d2.b	$$⊢\phi \to B\in W$$
3		wdom2d2.c	$$⊢\phi \to C\in X$$
4		wdom2d2.o	$$⊢\left(\phi \wedge x\in A\right)\to \exists y\in B\exists z\in Cx=X$$
5	2 3	xpexd	$$⊢\phi \to B\times C\in \mathrm{V}$$
6		nfcsb1v	$$⊢\underset{\_}{Ⅎ}y⦋1^{st}\left(w\right)/y⦌⦋2^{nd}\left(w\right)/z⦌X$$
7	6	nfeq2	$$⊢Ⅎyx=⦋1^{st}\left(w\right)/y⦌⦋2^{nd}\left(w\right)/z⦌X$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}z{1}^{st}\left(w\right)$$
9		nfcsb1v	$$⊢\underset{\_}{Ⅎ}z⦋2^{nd}\left(w\right)/z⦌X$$
10	8 9	nfcsbw	$$⊢\underset{\_}{Ⅎ}z⦋1^{st}\left(w\right)/y⦌⦋2^{nd}\left(w\right)/z⦌X$$
11	10	nfeq2	$$⊢Ⅎzx=⦋1^{st}\left(w\right)/y⦌⦋2^{nd}\left(w\right)/z⦌X$$
12		nfv	$$⊢Ⅎwx=X$$
13		csbopeq1a	$$⊢w=⟨y,z⟩\to ⦋1^{st}\left(w\right)/y⦌⦋2^{nd}\left(w\right)/z⦌X=X$$
14	13	eqeq2d	$$⊢w=⟨y,z⟩\to \left(x=⦋1^{st}\left(w\right)/y⦌⦋2^{nd}\left(w\right)/z⦌X\leftrightarrow x=X\right)$$
15	7 11 12 14	rexxpf	$$⊢\exists w\in \left(B\times C\right)x=⦋1^{st}\left(w\right)/y⦌⦋2^{nd}\left(w\right)/z⦌X\leftrightarrow \exists y\in B\exists z\in Cx=X$$
16	4 15	sylibr	$$⊢\left(\phi \wedge x\in A\right)\to \exists w\in \left(B\times C\right)x=⦋1^{st}\left(w\right)/y⦌⦋2^{nd}\left(w\right)/z⦌X$$
17	1 5 16	wdom2d	$$⊢\phi \to A{\preccurlyeq }^{*}\left(B\times C\right)$$