Theorem frpoins3xp3g

Description: Special case of founded partial recursion over a triple Cartesian 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		el2xptp	$$⊢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		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$$
38		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)$$
39	37 38	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)$$
40	39	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)$$
41	40	bicomi	$$⊢q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨x,y,z⟩\right)\leftrightarrow 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)$$
42		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)$$
43	41 42	bitri	$$⊢q\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨x,y,z⟩\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)$$
44	43	imbi1i	$$⊢\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(\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)$$
45		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)$$
46	44 45	bitri	$$⊢\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(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)$$
47	46	albii	$$⊢\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)\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)$$
48	47	bicomi	$$⊢\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)$$
49		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)$$
50		nfv	$$⊢Ⅎwq\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨x,y,z⟩\right)$$
51		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$$
52	50 51	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)$$
53		nfv	$$⊢Ⅎtq\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨x,y,z⟩\right)$$
54		nfcv	$$⊢\underset{\_}{Ⅎ}t{1}^{st}\left(1^{st}\left(q\right)\right)$$
55		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$$
56	54 55	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$$
57	53 56	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)$$
58		nfv	$$⊢Ⅎuq\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨x,y,z⟩\right)$$
59		nfcv	$$⊢\underset{\_}{Ⅎ}u{1}^{st}\left(1^{st}\left(q\right)\right)$$
60		nfcv	$$⊢\underset{\_}{Ⅎ}u{2}^{nd}\left(1^{st}\left(q\right)\right)$$
61		nfsbc1v	$$⊢Ⅎu\underset{\dot{}}{[}{2}^{nd}\left(q\right)/u\underset{\dot{}}{]}\theta$$
62	60 61	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$$
63	59 62	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$$
64	58 63	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)$$
65		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)$$
66		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)$$
67		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)$$
68	66 67	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)$$
69	52 57 64 65 68	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)$$
70		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)$$
71	39	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)$$
72		otelxp	$$⊢⟨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)$$
73	72	anbi1i	$$⊢\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 \left(\left(w\in A\wedge t\in B\wedge u\in C\right)\wedge ⟨w,t,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨x,y,z⟩\right)\right)$$
74	70 71 73	3bitr3i	$$⊢⟨w,t,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨x,y,z⟩\right)\leftrightarrow \left(\left(w\in A\wedge t\in B\wedge u\in C\right)\wedge ⟨w,t,u⟩\in Pred\left(R,\left(\left(A\times B\right)\times C\right),⟨x,y,z⟩\right)\right)$$
75	74	imbi1i	$$⊢\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(\left(w\in A\wedge t\in B\wedge u\in 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)$$
76		impexp	$$⊢\left(\left(\left(w\in A\wedge t\in B\wedge u\in 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(\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	75 76	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)$$
78	77	3albii	$$⊢\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	49 69 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	48 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	biimtrid	$$⊢\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	biimtrid	$$⊢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$$