Theorem frpoins3xpg

Description: Special case of founded partial induction over a Cartesian product. (Contributed by Scott Fenton, 22-Aug-2024)

	Ref	Expression
Hypotheses	frpoins3xpg.1	$$⊢\left(x\in A\wedge y\in B\right)\to \left(\forall z\forall w\left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\to \phi \right)$$
	frpoins3xpg.2	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
	frpoins3xpg.3	$$⊢y=w\to \left(\psi \leftrightarrow \chi \right)$$
	frpoins3xpg.4	$$⊢x=X\to \left(\phi \leftrightarrow \theta \right)$$
	frpoins3xpg.5	$$⊢y=Y\to \left(\theta \leftrightarrow \tau \right)$$
Assertion	frpoins3xpg	$$⊢\left(\left(R\mathrm{Fr}\left(A\times B\right)\wedge R\mathrm{Po}\left(A\times B\right)\wedge R\mathrm{Se}\left(A\times B\right)\right)\wedge \left(X\in A\wedge Y\in B\right)\right)\to \tau$$

Proof

Step	Hyp	Ref	Expression
1		frpoins3xpg.1	$$⊢\left(x\in A\wedge y\in B\right)\to \left(\forall z\forall w\left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\to \phi \right)$$
2		frpoins3xpg.2	$$⊢x=z\to \left(\phi \leftrightarrow \psi \right)$$
3		frpoins3xpg.3	$$⊢y=w\to \left(\psi \leftrightarrow \chi \right)$$
4		frpoins3xpg.4	$$⊢x=X\to \left(\phi \leftrightarrow \theta \right)$$
5		frpoins3xpg.5	$$⊢y=Y\to \left(\theta \leftrightarrow \tau \right)$$
6		elxp2	$$⊢p\in \left(A\times B\right)\leftrightarrow \exists x\in A\exists y\in Bp=⟨x,y⟩$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xPred\left(R,\left(A\times B\right),p\right)$$
8		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi$$
9	7 8	nfralw	$$⊢Ⅎx\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi$$
10		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi$$
11	9 10	nfim	$$⊢Ⅎx\left(\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \right)$$
12		nfv	$$⊢Ⅎyx\in A$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}yPred\left(R,\left(A\times B\right),p\right)$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}y{1}^{st}\left(q\right)$$
15		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi$$
16	14 15	nfsbcw	$$⊢Ⅎy\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi$$
17	13 16	nfralw	$$⊢Ⅎy\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi$$
18		nfcv	$$⊢\underset{\_}{Ⅎ}y{1}^{st}\left(p\right)$$
19		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi$$
20	18 19	nfsbcw	$$⊢Ⅎy\underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi$$
21	17 20	nfim	$$⊢Ⅎy\left(\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \right)$$
22	2	sbcbidv	$$⊢x=z\to \left(\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\psi \right)$$
23	22	cbvsbcvw	$$⊢\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\psi$$
24	3	cbvsbcvw	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi$$
25	24	sbcbii	$$⊢\underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi$$
26	23 25	bitri	$$⊢\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi$$
27	26	ralbii	$$⊢\forall q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \forall q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi$$
28		impexp	$$⊢\left(\left(q\in \left(A\times B\right)\wedge q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\leftrightarrow \left(q\in \left(A\times B\right)\to \left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\right)$$
29		elin	$$⊢q\in \left(\left(A\times B\right)\cap Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\leftrightarrow \left(q\in \left(A\times B\right)\wedge q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)$$
30		predss	$$⊢Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\subseteq A\times B$$
31		sseqin2	$$⊢Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\subseteq A\times B\leftrightarrow \left(A\times B\right)\cap Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)=Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)$$
32	30 31	mpbi	$$⊢\left(A\times B\right)\cap Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)=Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)$$
33	32	eleq2i	$$⊢q\in \left(\left(A\times B\right)\cap Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\leftrightarrow q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)$$
34	29 33	bitr3i	$$⊢\left(q\in \left(A\times B\right)\wedge q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\leftrightarrow q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)$$
35	34	imbi1i	$$⊢\left(\left(q\in \left(A\times B\right)\wedge q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\leftrightarrow \left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)$$
36	28 35	bitr3i	$$⊢\left(q\in \left(A\times B\right)\to \left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\right)\leftrightarrow \left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)$$
37	36	albii	$$⊢\forall q\left(q\in \left(A\times B\right)\to \left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\right)\leftrightarrow \forall q\left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)$$
38		df-ral	$$⊢\forall q\in \left(A\times B\right)\left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\leftrightarrow \forall q\left(q\in \left(A\times B\right)\to \left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\right)$$
39		df-ral	$$⊢\forall q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \leftrightarrow \forall q\left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)$$
40	37 38 39	3bitr4ri	$$⊢\forall q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \leftrightarrow \forall q\in \left(A\times B\right)\left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)$$
41		nfv	$$⊢Ⅎzq\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)$$
42		nfsbc1v	$$⊢Ⅎz\underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi$$
43	41 42	nfim	$$⊢Ⅎz\left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)$$
44		nfv	$$⊢Ⅎwq\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)$$
45		nfcv	$$⊢\underset{\_}{Ⅎ}w{1}^{st}\left(q\right)$$
46		nfsbc1v	$$⊢Ⅎw\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi$$
47	45 46	nfsbcw	$$⊢Ⅎw\underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi$$
48	44 47	nfim	$$⊢Ⅎw\left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)$$
49		nfv	$$⊢Ⅎq\left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)$$
50		eleq1	$$⊢q=⟨z,w⟩\to \left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\leftrightarrow ⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)$$
51		sbcopeq1a	$$⊢q=⟨z,w⟩\to \left(\underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \leftrightarrow \chi \right)$$
52	50 51	imbi12d	$$⊢q=⟨z,w⟩\to \left(\left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\leftrightarrow \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\right)$$
53	43 48 49 52	ralxpf	$$⊢\forall q\in \left(A\times B\right)\left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\leftrightarrow \forall z\in A\forall w\in B\left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)$$
54		r2al	$$⊢\forall z\in A\forall w\in B\left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\leftrightarrow \forall z\forall w\left(\left(z\in A\wedge w\in B\right)\to \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\right)$$
55		impexp	$$⊢\left(\left(⟨z,w⟩\in \left(A\times B\right)\wedge ⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\to \chi \right)\leftrightarrow \left(⟨z,w⟩\in \left(A\times B\right)\to \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\right)$$
56		opelxp	$$⊢⟨z,w⟩\in \left(A\times B\right)\leftrightarrow \left(z\in A\wedge w\in B\right)$$
57	56	imbi1i	$$⊢\left(⟨z,w⟩\in \left(A\times B\right)\to \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\right)\leftrightarrow \left(\left(z\in A\wedge w\in B\right)\to \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\right)$$
58	55 57	bitri	$$⊢\left(\left(⟨z,w⟩\in \left(A\times B\right)\wedge ⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\to \chi \right)\leftrightarrow \left(\left(z\in A\wedge w\in B\right)\to \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\right)$$
59		elin	$$⊢⟨z,w⟩\in \left(\left(A\times B\right)\cap Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\leftrightarrow \left(⟨z,w⟩\in \left(A\times B\right)\wedge ⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)$$
60	32	eleq2i	$$⊢⟨z,w⟩\in \left(\left(A\times B\right)\cap Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\leftrightarrow ⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)$$
61	59 60	bitr3i	$$⊢\left(⟨z,w⟩\in \left(A\times B\right)\wedge ⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\leftrightarrow ⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)$$
62	61	imbi1i	$$⊢\left(\left(⟨z,w⟩\in \left(A\times B\right)\wedge ⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\right)\to \chi \right)\leftrightarrow \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)$$
63	58 62	bitr3i	$$⊢\left(\left(z\in A\wedge w\in B\right)\to \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\right)\leftrightarrow \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)$$
64	63	2albii	$$⊢\forall z\forall w\left(\left(z\in A\wedge w\in B\right)\to \left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)\right)\leftrightarrow \forall z\forall w\left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)$$
65	53 54 64	3bitri	$$⊢\forall q\in \left(A\times B\right)\left(q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(q\right)/z\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/w\underset{\dot{}}{]}\chi \right)\leftrightarrow \forall z\forall w\left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)$$
66	27 40 65	3bitri	$$⊢\forall q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \forall z\forall w\left(⟨z,w⟩\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\to \chi \right)$$
67	66 1	biimtrid	$$⊢\left(x\in A\wedge y\in B\right)\to \left(\forall q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \phi \right)$$
68		predeq3	$$⊢p=⟨x,y⟩\to Pred\left(R,\left(A\times B\right),p\right)=Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)$$
69	68	raleqdv	$$⊢p=⟨x,y⟩\to \left(\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \forall q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \right)$$
70		sbcopeq1a	$$⊢p=⟨x,y⟩\to \left(\underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
71	69 70	imbi12d	$$⊢p=⟨x,y⟩\to \left(\left(\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\forall q\in Pred\left(R,\left(A\times B\right),⟨x,y⟩\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \phi \right)\right)$$
72	67 71	syl5ibrcom	$$⊢\left(x\in A\wedge y\in B\right)\to \left(p=⟨x,y⟩\to \left(\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \right)\right)$$
73	72	ex	$$⊢x\in A\to \left(y\in B\to \left(p=⟨x,y⟩\to \left(\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \right)\right)\right)$$
74	12 21 73	rexlimd	$$⊢x\in A\to \left(\exists y\in Bp=⟨x,y⟩\to \left(\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \right)\right)$$
75	11 74	rexlimi	$$⊢\exists x\in A\exists y\in Bp=⟨x,y⟩\to \left(\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \right)$$
76	6 75	sylbi	$$⊢p\in \left(A\times B\right)\to \left(\forall q\in Pred\left(R,\left(A\times B\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \right)$$
77		fveq2	$$⊢p=q\to 1^{st}\left(p\right)=1^{st}\left(q\right)$$
78		fveq2	$$⊢p=q\to 2^{nd}\left(p\right)=2^{nd}\left(q\right)$$
79	78	sbceq1d	$$⊢p=q\to \left(\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \right)$$
80	77 79	sbceqbid	$$⊢p=q\to \left(\underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(q\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/y\underset{\dot{}}{]}\phi \right)$$
81	76 80	frpoins2g	$$⊢\left(R\mathrm{Fr}\left(A\times B\right)\wedge R\mathrm{Po}\left(A\times B\right)\wedge R\mathrm{Se}\left(A\times B\right)\right)\to \forall p\in \left(A\times B\right)\underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi$$
82		ralxpes	$$⊢\forall p\in \left(A\times B\right)\underset{\dot{}}{[}{1}^{st}\left(p\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/y\underset{\dot{}}{]}\phi \leftrightarrow \forall x\in A\forall y\in B\phi$$
83	81 82	sylib	$$⊢\left(R\mathrm{Fr}\left(A\times B\right)\wedge R\mathrm{Po}\left(A\times B\right)\wedge R\mathrm{Se}\left(A\times B\right)\right)\to \forall x\in A\forall y\in B\phi$$
84	4 5	rspc2va	$$⊢\left(\left(X\in A\wedge Y\in B\right)\wedge \forall x\in A\forall y\in B\phi \right)\to \tau$$
85	83 84	sylan2	$$⊢\left(\left(X\in A\wedge Y\in B\right)\wedge \left(R\mathrm{Fr}\left(A\times B\right)\wedge R\mathrm{Po}\left(A\times B\right)\wedge R\mathrm{Se}\left(A\times B\right)\right)\right)\to \tau$$
86	85	ancoms	$$⊢\left(\left(R\mathrm{Fr}\left(A\times B\right)\wedge R\mathrm{Po}\left(A\times B\right)\wedge R\mathrm{Se}\left(A\times B\right)\right)\wedge \left(X\in A\wedge Y\in B\right)\right)\to \tau$$