Metamath Proof Explorer

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 
|- ( ( x e. A /\ y e. B /\ z e. C ) -> ( A. w A. t A. u ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) -> ph ) )
frpoins3xp3g.2 
|- ( x = w -> ( ph <-> ps ) )
frpoins3xp3g.3 
|- ( y = t -> ( ps <-> ch ) )
frpoins3xp3g.4 
|- ( z = u -> ( ch <-> th ) )
frpoins3xp3g.5 
|- ( x = X -> ( ph <-> ta ) )
frpoins3xp3g.6 
|- ( y = Y -> ( ta <-> et ) )
frpoins3xp3g.7 
|- ( z = Z -> ( et <-> ze ) )
Assertion frpoins3xp3g 
|- ( ( ( R Fr ( ( A X. B ) X. C ) /\ R Po ( ( A X. B ) X. C ) /\ R Se ( ( A X. B ) X. C ) ) /\ ( X e. A /\ Y e. B /\ Z e. C ) ) -> ze )

Proof

Step Hyp Ref Expression
1 frpoins3xp3g.1 
 |-  ( ( x e. A /\ y e. B /\ z e. C ) -> ( A. w A. t A. u ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) -> ph ) )
2 frpoins3xp3g.2 
 |-  ( x = w -> ( ph <-> ps ) )
3 frpoins3xp3g.3 
 |-  ( y = t -> ( ps <-> ch ) )
4 frpoins3xp3g.4 
 |-  ( z = u -> ( ch <-> th ) )
5 frpoins3xp3g.5 
 |-  ( x = X -> ( ph <-> ta ) )
6 frpoins3xp3g.6 
 |-  ( y = Y -> ( ta <-> et ) )
7 frpoins3xp3g.7 
 |-  ( z = Z -> ( et <-> ze ) )
8 2 sbcbidv 
 |-  ( x = w -> ( [. ( 2nd ` q ) / z ]. ph <-> [. ( 2nd ` q ) / z ]. ps ) )
9 8 sbcbidv 
 |-  ( x = w -> ( [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ph <-> [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ps ) )
10 9 cbvsbcvw 
 |-  ( [. ( 1st ` ( 1st ` q ) ) / x ]. [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ph <-> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ps )
11 3 sbcbidv 
 |-  ( y = t -> ( [. ( 2nd ` q ) / z ]. ps <-> [. ( 2nd ` q ) / z ]. ch ) )
12 11 cbvsbcvw 
 |-  ( [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ps <-> [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / z ]. ch )
13 4 cbvsbcvw 
 |-  ( [. ( 2nd ` q ) / z ]. ch <-> [. ( 2nd ` q ) / u ]. th )
14 13 sbcbii 
 |-  ( [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / z ]. ch <-> [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th )
15 12 14 bitri 
 |-  ( [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ps <-> [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th )
16 15 sbcbii 
 |-  ( [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ps <-> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th )
17 10 16 bitri 
 |-  ( [. ( 1st ` ( 1st ` q ) ) / x ]. [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ph <-> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th )
18 17 ralbii 
 |-  ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / x ]. [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ph <-> A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th )
19 elxpxp 
 |-  ( p e. ( ( A X. B ) X. C ) <-> E. x e. A E. y e. B E. z e. C p = <. <. x , y >. , z >. )
20 nfv 
 |-  F/ x A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
21 nfsbc1v 
 |-  F/ x [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph
22 20 21 nfim 
 |-  F/ x ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph )
23 nfv 
 |-  F/ y x e. A
24 nfv 
 |-  F/ y A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
25 nfcv 
 |-  F/_ y ( 1st ` ( 1st ` p ) )
26 nfsbc1v 
 |-  F/ y [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph
27 25 26 nfsbcw 
 |-  F/ y [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph
28 24 27 nfim 
 |-  F/ y ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph )
29 nfv 
 |-  F/ z ( x e. A /\ y e. B )
30 nfv 
 |-  F/ z A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
31 nfcv 
 |-  F/_ z ( 1st ` ( 1st ` p ) )
32 nfcv 
 |-  F/_ z ( 2nd ` ( 1st ` p ) )
33 nfsbc1v 
 |-  F/ z [. ( 2nd ` p ) / z ]. ph
34 32 33 nfsbcw 
 |-  F/ z [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph
35 31 34 nfsbcw 
 |-  F/ z [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph
36 30 35 nfim 
 |-  F/ z ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph )
37 impexp 
 |-  ( ( ( q e. ( ( A X. B ) X. C ) /\ q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) <-> ( q e. ( ( A X. B ) X. C ) -> ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) ) )
38 elin 
 |-  ( q e. ( ( ( A X. B ) X. C ) i^i Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) <-> ( q e. ( ( A X. B ) X. C ) /\ q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) )
39 predss 
 |-  Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) C_ ( ( A X. B ) X. C )
40 sseqin2 
 |-  ( Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) C_ ( ( A X. B ) X. C ) <-> ( ( ( A X. B ) X. C ) i^i Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) = Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) )
41 39 40 mpbi 
 |-  ( ( ( A X. B ) X. C ) i^i Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) = Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. )
42 41 eleq2i 
 |-  ( q e. ( ( ( A X. B ) X. C ) i^i Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) <-> q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) )
43 38 42 bitr3i 
 |-  ( ( q e. ( ( A X. B ) X. C ) /\ q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) <-> q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) )
44 43 imbi1i 
 |-  ( ( ( q e. ( ( A X. B ) X. C ) /\ q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) <-> ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) )
45 37 44 bitr3i 
 |-  ( ( q e. ( ( A X. B ) X. C ) -> ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) ) <-> ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) )
46 45 albii 
 |-  ( A. q ( q e. ( ( A X. B ) X. C ) -> ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) ) <-> A. q ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) )
47 r3al 
 |-  ( A. w e. A A. t e. B A. u e. C ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) <-> A. w A. t A. u ( ( w e. A /\ t e. B /\ u e. C ) -> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) ) )
48 nfv 
 |-  F/ w q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. )
49 nfsbc1v 
 |-  F/ w [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
50 48 49 nfim 
 |-  F/ w ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th )
51 nfv 
 |-  F/ t q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. )
52 nfcv 
 |-  F/_ t ( 1st ` ( 1st ` q ) )
53 nfsbc1v 
 |-  F/ t [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
54 52 53 nfsbcw 
 |-  F/ t [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
55 51 54 nfim 
 |-  F/ t ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th )
56 nfv 
 |-  F/ u q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. )
57 nfcv 
 |-  F/_ u ( 1st ` ( 1st ` q ) )
58 nfcv 
 |-  F/_ u ( 2nd ` ( 1st ` q ) )
59 nfsbc1v 
 |-  F/ u [. ( 2nd ` q ) / u ]. th
60 58 59 nfsbcw 
 |-  F/ u [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
61 57 60 nfsbcw 
 |-  F/ u [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
62 56 61 nfim 
 |-  F/ u ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th )
63 nfv 
 |-  F/ q ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th )
64 eleq1 
 |-  ( q = <. <. w , t >. , u >. -> ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) <-> <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) )
65 sbcoteq1a 
 |-  ( q = <. <. w , t >. , u >. -> ( [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th <-> th ) )
66 64 65 imbi12d 
 |-  ( q = <. <. w , t >. , u >. -> ( ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) <-> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) ) )
67 50 55 62 63 66 ralxp3f 
 |-  ( A. q e. ( ( A X. B ) X. C ) ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) <-> A. w e. A A. t e. B A. u e. C ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) )
68 elin 
 |-  ( <. <. w , t >. , u >. e. ( ( ( A X. B ) X. C ) i^i Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) <-> ( <. <. w , t >. , u >. e. ( ( A X. B ) X. C ) /\ <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) )
69 41 eleq2i 
 |-  ( <. <. w , t >. , u >. e. ( ( ( A X. B ) X. C ) i^i Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) <-> <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) )
70 68 69 bitr3i 
 |-  ( ( <. <. w , t >. , u >. e. ( ( A X. B ) X. C ) /\ <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) <-> <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) )
71 70 imbi1i 
 |-  ( ( ( <. <. w , t >. , u >. e. ( ( A X. B ) X. C ) /\ <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) -> th ) <-> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) )
72 impexp 
 |-  ( ( ( <. <. w , t >. , u >. e. ( ( A X. B ) X. C ) /\ <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) ) -> th ) <-> ( <. <. w , t >. , u >. e. ( ( A X. B ) X. C ) -> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) ) )
73 71 72 bitr3i 
 |-  ( ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) <-> ( <. <. w , t >. , u >. e. ( ( A X. B ) X. C ) -> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) ) )
74 ot2elxp 
 |-  ( <. <. w , t >. , u >. e. ( ( A X. B ) X. C ) <-> ( w e. A /\ t e. B /\ u e. C ) )
75 74 imbi1i 
 |-  ( ( <. <. w , t >. , u >. e. ( ( A X. B ) X. C ) -> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) ) <-> ( ( w e. A /\ t e. B /\ u e. C ) -> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) ) )
76 73 75 bitri 
 |-  ( ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) <-> ( ( w e. A /\ t e. B /\ u e. C ) -> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) ) )
77 76 albii 
 |-  ( A. u ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) <-> A. u ( ( w e. A /\ t e. B /\ u e. C ) -> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) ) )
78 77 2albii 
 |-  ( A. w A. t A. u ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) <-> A. w A. t A. u ( ( w e. A /\ t e. B /\ u e. C ) -> ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) ) )
79 47 67 78 3bitr4ri 
 |-  ( A. w A. t A. u ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) <-> A. q e. ( ( A X. B ) X. C ) ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) )
80 df-ral 
 |-  ( A. q e. ( ( A X. B ) X. C ) ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) <-> A. q ( q e. ( ( A X. B ) X. C ) -> ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) ) )
81 79 80 bitri 
 |-  ( A. w A. t A. u ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) <-> A. q ( q e. ( ( A X. B ) X. C ) -> ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) ) )
82 df-ral 
 |-  ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th <-> A. q ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) )
83 46 81 82 3bitr4ri 
 |-  ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th <-> A. w A. t A. u ( <. <. w , t >. , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) -> th ) )
84 83 1 syl5bi 
 |-  ( ( x e. A /\ y e. B /\ z e. C ) -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> ph ) )
85 predeq3 
 |-  ( p = <. <. x , y >. , z >. -> Pred ( R , ( ( A X. B ) X. C ) , p ) = Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) )
86 85 raleqdv 
 |-  ( p = <. <. x , y >. , z >. -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th <-> A. q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th ) )
87 sbcoteq1a 
 |-  ( p = <. <. x , y >. , z >. -> ( [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph <-> ph ) )
88 86 87 imbi12d 
 |-  ( p = <. <. x , y >. , z >. -> ( ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph ) <-> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , <. <. x , y >. , z >. ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> ph ) ) )
89 84 88 syl5ibrcom 
 |-  ( ( x e. A /\ y e. B /\ z e. C ) -> ( p = <. <. x , y >. , z >. -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph ) ) )
90 89 3expia 
 |-  ( ( x e. A /\ y e. B ) -> ( z e. C -> ( p = <. <. x , y >. , z >. -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph ) ) ) )
91 29 36 90 rexlimd 
 |-  ( ( x e. A /\ y e. B ) -> ( E. z e. C p = <. <. x , y >. , z >. -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph ) ) )
92 91 ex 
 |-  ( x e. A -> ( y e. B -> ( E. z e. C p = <. <. x , y >. , z >. -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph ) ) ) )
93 23 28 92 rexlimd 
 |-  ( x e. A -> ( E. y e. B E. z e. C p = <. <. x , y >. , z >. -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph ) ) )
94 22 93 rexlimi 
 |-  ( E. x e. A E. y e. B E. z e. C p = <. <. x , y >. , z >. -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph ) )
95 19 94 sylbi 
 |-  ( p e. ( ( A X. B ) X. C ) -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph ) )
96 18 95 syl5bi 
 |-  ( p e. ( ( A X. B ) X. C ) -> ( A. q e. Pred ( R , ( ( A X. B ) X. C ) , p ) [. ( 1st ` ( 1st ` q ) ) / x ]. [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ph -> [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph ) )
97 2fveq3 
 |-  ( p = q -> ( 1st ` ( 1st ` p ) ) = ( 1st ` ( 1st ` q ) ) )
98 2fveq3 
 |-  ( p = q -> ( 2nd ` ( 1st ` p ) ) = ( 2nd ` ( 1st ` q ) ) )
99 fveq2 
 |-  ( p = q -> ( 2nd ` p ) = ( 2nd ` q ) )
100 99 sbceq1d 
 |-  ( p = q -> ( [. ( 2nd ` p ) / z ]. ph <-> [. ( 2nd ` q ) / z ]. ph ) )
101 98 100 sbceqbid 
 |-  ( p = q -> ( [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph <-> [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ph ) )
102 97 101 sbceqbid 
 |-  ( p = q -> ( [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph <-> [. ( 1st ` ( 1st ` q ) ) / x ]. [. ( 2nd ` ( 1st ` q ) ) / y ]. [. ( 2nd ` q ) / z ]. ph ) )
103 96 102 frpoins2g 
 |-  ( ( R Fr ( ( A X. B ) X. C ) /\ R Po ( ( A X. B ) X. C ) /\ R Se ( ( A X. B ) X. C ) ) -> A. p e. ( ( A X. B ) X. C ) [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph )
104 ralxp3es 
 |-  ( A. p e. ( ( A X. B ) X. C ) [. ( 1st ` ( 1st ` p ) ) / x ]. [. ( 2nd ` ( 1st ` p ) ) / y ]. [. ( 2nd ` p ) / z ]. ph <-> A. x e. A A. y e. B A. z e. C ph )
105 103 104 sylib 
 |-  ( ( R Fr ( ( A X. B ) X. C ) /\ R Po ( ( A X. B ) X. C ) /\ R Se ( ( A X. B ) X. C ) ) -> A. x e. A A. y e. B A. z e. C ph )
106 5 6 7 rspc3v 
 |-  ( ( X e. A /\ Y e. B /\ Z e. C ) -> ( A. x e. A A. y e. B A. z e. C ph -> ze ) )
107 105 106 mpan9 
 |-  ( ( ( R Fr ( ( A X. B ) X. C ) /\ R Po ( ( A X. B ) X. C ) /\ R Se ( ( A X. B ) X. C ) ) /\ ( X e. A /\ Y e. B /\ Z e. C ) ) -> ze )