Theorem frpoins3xp3g

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

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

Proof

Step	Hyp	Ref	Expression
1		frpoins3xp3g.1	$$⊢\left(x\in A\wedge y\in B\wedge z\in C\right)\to \left(\forall w\forall t\forall u\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\to \phi \right)$$
2		frpoins3xp3g.2	$$⊢x=w\to \left(\phi \leftrightarrow \psi \right)$$
3		frpoins3xp3g.3	$$⊢y=t\to \left(\psi \leftrightarrow \chi \right)$$
4		frpoins3xp3g.4	$$⊢z=u\to \left(\chi \leftrightarrow \theta \right)$$
5		frpoins3xp3g.5	$$⊢x=X\to \left(\phi \leftrightarrow \tau \right)$$
6		frpoins3xp3g.6	$$⊢y=Y\to \left(\tau \leftrightarrow \eta \right)$$
7		frpoins3xp3g.7	$$⊢z=Z\to \left(\eta \leftrightarrow \zeta \right)$$
8	2	sbcbidv	$$⊢x=w\to \left(\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\psi \right)$$
9	8	sbcbidv	$$⊢x=w\to \left(\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\psi \right)$$
10	9	cbvsbcvw	$$⊢\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\psi$$
11	3	sbcbidv	$$⊢y=t\to \left(\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\chi \right)$$
12	11	cbvsbcvw	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\chi$$
13	4	cbvsbcvw	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
14	13	sbcbii	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\chi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
15	12 14	bitri	$$⊢\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
16	15	sbcbii	$$⊢\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\psi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
17	10 16	bitri	$$⊢\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
18	17	ralbii	$$⊢\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
19		elxpxp	$$⊢p\in \left(\left(A\times B\right)\times C\right)\leftrightarrow \exists x\in A\exists y\in B\exists z\in Cp=⟨⟨x,y⟩,z⟩$$
20		nfv	$$⊢Ⅎx\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
21		nfsbc1v	$$⊢Ⅎx\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi$$
22	20 21	nfim	$$⊢Ⅎx\left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)$$
23		nfv	$$⊢Ⅎyx\in A$$
24		nfv	$$⊢Ⅎy\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}y{1}^{st}\left(1^{st}\left(p\right)\right)$$
26		nfsbc1v	$$⊢Ⅎy\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi$$
27	25 26	nfsbcw	$$⊢Ⅎy\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi$$
28	24 27	nfim	$$⊢Ⅎy\left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)$$
29		nfv	$$⊢Ⅎz\left(x\in A\wedge y\in B\right)$$
30		nfv	$$⊢Ⅎz\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
31		nfcv	$$⊢\underset{\_}{Ⅎ}z{1}^{st}\left(1^{st}\left(p\right)\right)$$
32		nfcv	$$⊢\underset{\_}{Ⅎ}z{2}^{nd}\left(1^{st}\left(p\right)\right)$$
33		nfsbc1v	$$⊢Ⅎz\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi$$
34	32 33	nfsbcw	$$⊢Ⅎz\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi$$
35	31 34	nfsbcw	$$⊢Ⅎz\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi$$
36	30 35	nfim	$$⊢Ⅎz\left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)$$
37		impexp	$$⊢\left(\left(q\in \left(\left(A\times B\right)\times C\right)\wedge q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\leftrightarrow \left(q\in \left(\left(A\times B\right)\times C\right)\to \left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\right)$$
38		elin	$$⊢q\in \left(\left(\left(A\times B\right)\times C\right)\cap Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\leftrightarrow \left(q\in \left(\left(A\times B\right)\times C\right)\wedge q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)$$
39		predss	$$⊢Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\subseteq \left(A\times B\right)\times C$$
40		sseqin2	$$⊢Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\subseteq \left(A\times B\right)\times C\leftrightarrow \left(\left(A\times B\right)\times C\right)\cap Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)=Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
41	39 40	mpbi	$$⊢\left(\left(A\times B\right)\times C\right)\cap Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)=Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
42	41	eleq2i	$$⊢q\in \left(\left(\left(A\times B\right)\times C\right)\cap Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\leftrightarrow q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
43	38 42	bitr3i	$$⊢\left(q\in \left(\left(A\times B\right)\times C\right)\wedge q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\leftrightarrow q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
44	43	imbi1i	$$⊢\left(\left(q\in \left(\left(A\times B\right)\times C\right)\wedge q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\leftrightarrow \left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)$$
45	37 44	bitr3i	$$⊢\left(q\in \left(\left(A\times B\right)\times C\right)\to \left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\right)\leftrightarrow \left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)$$
46	45	albii	$$⊢\forall q\left(q\in \left(\left(A\times B\right)\times C\right)\to \left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\right)\leftrightarrow \forall q\left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)$$
47		r3al	$$⊢\forall w\in A\forall t\in B\forall u\in C\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\leftrightarrow \forall w\forall t\forall u\left(\left(w\in A\wedge t\in B\wedge u\in C\right)\to \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\right)$$
48		nfv	$$⊢Ⅎwq\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
49		nfsbc1v	$$⊢Ⅎw\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
50	48 49	nfim	$$⊢Ⅎw\left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)$$
51		nfv	$$⊢Ⅎtq\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
52		nfcv	$$⊢\underset{\_}{Ⅎ}t{1}^{st}\left(1^{st}\left(q\right)\right)$$
53		nfsbc1v	$$⊢Ⅎt\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
54	52 53	nfsbcw	$$⊢Ⅎt\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
55	51 54	nfim	$$⊢Ⅎt\left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)$$
56		nfv	$$⊢Ⅎuq\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
57		nfcv	$$⊢\underset{\_}{Ⅎ}u{1}^{st}\left(1^{st}\left(q\right)\right)$$
58		nfcv	$$⊢\underset{\_}{Ⅎ}u{2}^{nd}\left(1^{st}\left(q\right)\right)$$
59		nfsbc1v	$$⊢Ⅎu\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
60	58 59	nfsbcw	$$⊢Ⅎu\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
61	57 60	nfsbcw	$$⊢Ⅎu\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
62	56 61	nfim	$$⊢Ⅎu\left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)$$
63		nfv	$$⊢Ⅎq\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)$$
64		eleq1	$$⊢q=⟨⟨w,t⟩,u⟩\to \left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\leftrightarrow ⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)$$
65		sbcoteq1a	$$⊢q=⟨⟨w,t⟩,u⟩\to \left(\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \leftrightarrow \theta \right)$$
66	64 65	imbi12d	$$⊢q=⟨⟨w,t⟩,u⟩\to \left(\left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\leftrightarrow \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\right)$$
67	50 55 62 63 66	ralxp3f	$$⊢\forall q\in \left(\left(A\times B\right)\times C\right)\left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\leftrightarrow \forall w\in A\forall t\in B\forall u\in C\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)$$
68		elin	$$⊢⟨⟨w,t⟩,u⟩\in \left(\left(\left(A\times B\right)\times C\right)\cap Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\leftrightarrow \left(⟨⟨w,t⟩,u⟩\in \left(\left(A\times B\right)\times C\right)\wedge ⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)$$
69	41	eleq2i	$$⊢⟨⟨w,t⟩,u⟩\in \left(\left(\left(A\times B\right)\times C\right)\cap Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\leftrightarrow ⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
70	68 69	bitr3i	$$⊢\left(⟨⟨w,t⟩,u⟩\in \left(\left(A\times B\right)\times C\right)\wedge ⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\leftrightarrow ⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
71	70	imbi1i	$$⊢\left(\left(⟨⟨w,t⟩,u⟩\in \left(\left(A\times B\right)\times C\right)\wedge ⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\to \theta \right)\leftrightarrow \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)$$
72		impexp	$$⊢\left(\left(⟨⟨w,t⟩,u⟩\in \left(\left(A\times B\right)\times C\right)\wedge ⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\right)\to \theta \right)\leftrightarrow \left(⟨⟨w,t⟩,u⟩\in \left(\left(A\times B\right)\times C\right)\to \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\right)$$
73	71 72	bitr3i	$$⊢\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\leftrightarrow \left(⟨⟨w,t⟩,u⟩\in \left(\left(A\times B\right)\times C\right)\to \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\right)$$
74		ot2elxp	$$⊢⟨⟨w,t⟩,u⟩\in \left(\left(A\times B\right)\times C\right)\leftrightarrow \left(w\in A\wedge t\in B\wedge u\in C\right)$$
75	74	imbi1i	$$⊢\left(⟨⟨w,t⟩,u⟩\in \left(\left(A\times B\right)\times C\right)\to \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\right)\leftrightarrow \left(\left(w\in A\wedge t\in B\wedge u\in C\right)\to \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\right)$$
76	73 75	bitri	$$⊢\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\leftrightarrow \left(\left(w\in A\wedge t\in B\wedge u\in C\right)\to \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\right)$$
77	76	albii	$$⊢\forall u\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\leftrightarrow \forall u\left(\left(w\in A\wedge t\in B\wedge u\in C\right)\to \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\right)$$
78	77	2albii	$$⊢\forall w\forall t\forall u\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\leftrightarrow \forall w\forall t\forall u\left(\left(w\in A\wedge t\in B\wedge u\in C\right)\to \left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\right)$$
79	47 67 78	3bitr4ri	$$⊢\forall w\forall t\forall u\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\leftrightarrow \forall q\in \left(\left(A\times B\right)\times C\right)\left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)$$
80		df-ral	$$⊢\forall q\in \left(\left(A\times B\right)\times C\right)\left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\leftrightarrow \forall q\left(q\in \left(\left(A\times B\right)\times C\right)\to \left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\right)$$
81	79 80	bitri	$$⊢\forall w\forall t\forall u\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)\leftrightarrow \forall q\left(q\in \left(\left(A\times B\right)\times C\right)\to \left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)\right)$$
82		df-ral	$$⊢\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \leftrightarrow \forall q\left(q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)$$
83	46 81 82	3bitr4ri	$$⊢\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \leftrightarrow \forall w\forall t\forall u\left(⟨⟨w,t⟩,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\to \theta \right)$$
84	83 1	syl5bi	$$⊢\left(x\in A\wedge y\in B\wedge z\in C\right)\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \phi \right)$$
85		predeq3	$$⊢p=⟨⟨x,y⟩,z⟩\to Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)=Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)$$
86	85	raleqdv	$$⊢p=⟨⟨x,y⟩,z⟩\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \leftrightarrow \forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \right)$$
87		sbcoteq1a	$$⊢p=⟨⟨x,y⟩,z⟩\to \left(\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \phi \right)$$
88	86 87	imbi12d	$$⊢p=⟨⟨x,y⟩,z⟩\to \left(\left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)\leftrightarrow \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨⟨x,y⟩,z⟩\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \phi \right)\right)$$
89	84 88	syl5ibrcom	$$⊢\left(x\in A\wedge y\in B\wedge z\in C\right)\to \left(p=⟨⟨x,y⟩,z⟩\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)\right)$$
90	89	3expia	$$⊢\left(x\in A\wedge y\in B\right)\to \left(z\in C\to \left(p=⟨⟨x,y⟩,z⟩\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)\right)\right)$$
91	29 36 90	rexlimd	$$⊢\left(x\in A\wedge y\in B\right)\to \left(\exists z\in Cp=⟨⟨x,y⟩,z⟩\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)\right)$$
92	91	ex	$$⊢x\in A\to \left(y\in B\to \left(\exists z\in Cp=⟨⟨x,y⟩,z⟩\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)\right)\right)$$
93	23 28 92	rexlimd	$$⊢x\in A\to \left(\exists y\in B\exists z\in Cp=⟨⟨x,y⟩,z⟩\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)\right)$$
94	22 93	rexlimi	$$⊢\exists x\in A\exists y\in B\exists z\in Cp=⟨⟨x,y⟩,z⟩\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)$$
95	19 94	sylbi	$$⊢p\in \left(\left(A\times B\right)\times C\right)\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/w\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/t\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)$$
96	18 95	syl5bi	$$⊢p\in \left(\left(A\times B\right)\times C\right)\to \left(\forall q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),p\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\phi \to \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \right)$$
97		2fveq3	$$⊢p=q\to 1^{st}\left(1^{st}\left(p\right)\right)=1^{st}\left(1^{st}\left(q\right)\right)$$
98		2fveq3	$$⊢p=q\to 2^{nd}\left(1^{st}\left(p\right)\right)=2^{nd}\left(1^{st}\left(q\right)\right)$$
99		fveq2	$$⊢p=q\to 2^{nd}\left(p\right)=2^{nd}\left(q\right)$$
100	99	sbceq1d	$$⊢p=q\to \left(\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\phi \right)$$
101	98 100	sbceqbid	$$⊢p=q\to \left(\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\phi \right)$$
102	97 101	sbceqbid	$$⊢p=q\to \left(\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(q\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(q\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(q\right)/z\underset{\dot{}}{]}\phi \right)$$
103	96 102	frpoins2g	$$⊢\left(R\mathrm{Fr}\left(\left(A\times B\right)\times C\right)\wedge R\mathrm{Po}\left(\left(A\times B\right)\times C\right)\wedge R\mathrm{Se}\left(\left(A\times B\right)\times C\right)\right)\to \forall p\in \left(\left(A\times B\right)\times C\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi$$
104		ralxp3es	$$⊢\forall p\in \left(\left(A\times B\right)\times C\right)\underset{\dot{}}{[}{1}^{st}\left(1^{st}\left(p\right)\right)/x\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(1^{st}\left(p\right)\right)/y\underset{\dot{}}{]}\underset{\dot{}}{[}{2}^{nd}\left(p\right)/z\underset{\dot{}}{]}\phi \leftrightarrow \forall x\in A\forall y\in B\forall z\in C\phi$$
105	103 104	sylib	$$⊢\left(R\mathrm{Fr}\left(\left(A\times B\right)\times C\right)\wedge R\mathrm{Po}\left(\left(A\times B\right)\times C\right)\wedge R\mathrm{Se}\left(\left(A\times B\right)\times C\right)\right)\to \forall x\in A\forall y\in B\forall z\in C\phi$$
106	5 6 7	rspc3v	$$⊢\left(X\in A\wedge Y\in B\wedge Z\in C\right)\to \left(\forall x\in A\forall y\in B\forall z\in C\phi \to \zeta \right)$$
107	105 106	mpan9	$$⊢\left(\left(R\mathrm{Fr}\left(\left(A\times B\right)\times C\right)\wedge R\mathrm{Po}\left(\left(A\times B\right)\times C\right)\wedge R\mathrm{Se}\left(\left(A\times B\right)\times C\right)\right)\wedge \left(X\in A\wedge Y\in B\wedge Z\in C\right)\right)\to \zeta$$