Metamath Proof Explorer

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 
|- ( ( 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 el2xptp 
 |-  ( 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 predss 
 |-  Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. ) C_ ( ( A X. B ) X. C )
38 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 >. ) )
39 37 38 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 >. )
40 39 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 >. ) )
41 40 bicomi 
 |-  ( q e. Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. ) <-> q e. ( ( ( A X. B ) X. C ) i^i Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. ) ) )
42 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 >. ) ) )
43 41 42 bitri 
 |-  ( q e. 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 >. ) ) )
44 43 imbi1i 
 |-  ( ( 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 ) )
45 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 ) ) )
46 44 45 bitri 
 |-  ( ( 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 ) ) )
47 46 albii 
 |-  ( 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 ) <-> 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 ) ) )
48 47 bicomi 
 |-  ( 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 ) )
49 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 ) ) )
50 nfv 
 |-  F/ w q e. Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. )
51 nfsbc1v 
 |-  F/ w [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
52 50 51 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 )
53 nfv 
 |-  F/ t q e. Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. )
54 nfcv 
 |-  F/_ t ( 1st ` ( 1st ` q ) )
55 nfsbc1v 
 |-  F/ t [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
56 54 55 nfsbcw 
 |-  F/ t [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
57 53 56 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 )
58 nfv 
 |-  F/ u q e. Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. )
59 nfcv 
 |-  F/_ u ( 1st ` ( 1st ` q ) )
60 nfcv 
 |-  F/_ u ( 2nd ` ( 1st ` q ) )
61 nfsbc1v 
 |-  F/ u [. ( 2nd ` q ) / u ]. th
62 60 61 nfsbcw 
 |-  F/ u [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
63 59 62 nfsbcw 
 |-  F/ u [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th
64 58 63 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 )
65 nfv 
 |-  F/ q ( <. w , t , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. ) -> th )
66 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 >. ) ) )
67 sbcoteq1a 
 |-  ( q = <. w , t , u >. -> ( [. ( 1st ` ( 1st ` q ) ) / w ]. [. ( 2nd ` ( 1st ` q ) ) / t ]. [. ( 2nd ` q ) / u ]. th <-> th ) )
68 66 67 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 ) ) )
69 52 57 64 65 68 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 ) )
70 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 >. ) ) )
71 39 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 >. ) )
72 otelxp 
 |-  ( <. w , t , u >. e. ( ( A X. B ) X. C ) <-> ( w e. A /\ t e. B /\ u e. C ) )
73 72 anbi1i 
 |-  ( ( <. w , t , u >. e. ( ( A X. B ) X. C ) /\ <. w , t , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. ) ) <-> ( ( w e. A /\ t e. B /\ u e. C ) /\ <. w , t , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. ) ) )
74 70 71 73 3bitr3i 
 |-  ( <. w , t , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. ) <-> ( ( w e. A /\ t e. B /\ u e. C ) /\ <. w , t , u >. e. Pred ( R , ( ( A X. B ) X. C ) , <. x , y , z >. ) ) )
75 74 imbi1i 
 |-  ( ( <. 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 impexp 
 |-  ( ( ( ( w e. A /\ t e. B /\ u e. 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 ) ) )
77 75 76 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 ) ) )
78 77 3albii 
 |-  ( 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 49 69 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 48 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 biimtrid 
 |-  ( ( 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 biimtrid 
 |-  ( 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 )