Metamath Proof Explorer

Theorem frpoins3xpg

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

Ref Expression
Hypotheses frpoins3xpg.1 
|- ( ( x e. A /\ y e. B ) -> ( A. z A. w ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) -> ph ) )
frpoins3xpg.2 
|- ( x = z -> ( ph <-> ps ) )
frpoins3xpg.3 
|- ( y = w -> ( ps <-> ch ) )
frpoins3xpg.4 
|- ( x = X -> ( ph <-> th ) )
frpoins3xpg.5 
|- ( y = Y -> ( th <-> ta ) )
Assertion frpoins3xpg 
|- ( ( ( R Fr ( A X. B ) /\ R Po ( A X. B ) /\ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta )

Proof

Step Hyp Ref Expression
1 frpoins3xpg.1 
 |-  ( ( x e. A /\ y e. B ) -> ( A. z A. w ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) -> ph ) )
2 frpoins3xpg.2 
 |-  ( x = z -> ( ph <-> ps ) )
3 frpoins3xpg.3 
 |-  ( y = w -> ( ps <-> ch ) )
4 frpoins3xpg.4 
 |-  ( x = X -> ( ph <-> th ) )
5 frpoins3xpg.5 
 |-  ( y = Y -> ( th <-> ta ) )
6 elxp2 
 |-  ( p e. ( A X. B ) <-> E. x e. A E. y e. B p = <. x , y >. )
7 nfcv 
 |-  F/_ x Pred ( R , ( A X. B ) , p )
8 nfsbc1v 
 |-  F/ x [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph
9 7 8 nfralw 
 |-  F/ x A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph
10 nfsbc1v 
 |-  F/ x [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph
11 9 10 nfim 
 |-  F/ x ( A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph )
12 nfv 
 |-  F/ y x e. A
13 nfcv 
 |-  F/_ y Pred ( R , ( A X. B ) , p )
14 nfcv 
 |-  F/_ y ( 1st ` q )
15 nfsbc1v 
 |-  F/ y [. ( 2nd ` q ) / y ]. ph
16 14 15 nfsbcw 
 |-  F/ y [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph
17 13 16 nfralw 
 |-  F/ y A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph
18 nfcv 
 |-  F/_ y ( 1st ` p )
19 nfsbc1v 
 |-  F/ y [. ( 2nd ` p ) / y ]. ph
20 18 19 nfsbcw 
 |-  F/ y [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph
21 17 20 nfim 
 |-  F/ y ( A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph )
22 2 sbcbidv 
 |-  ( x = z -> ( [. ( 2nd ` q ) / y ]. ph <-> [. ( 2nd ` q ) / y ]. ps ) )
23 22 cbvsbcvw 
 |-  ( [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph <-> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / y ]. ps )
24 3 cbvsbcvw 
 |-  ( [. ( 2nd ` q ) / y ]. ps <-> [. ( 2nd ` q ) / w ]. ch )
25 24 sbcbii 
 |-  ( [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / y ]. ps <-> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch )
26 23 25 bitri 
 |-  ( [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph <-> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch )
27 26 ralbii 
 |-  ( A. q e. Pred ( R , ( A X. B ) , <. x , y >. ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph <-> A. q e. Pred ( R , ( A X. B ) , <. x , y >. ) [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch )
28 impexp 
 |-  ( ( ( q e. ( A X. B ) /\ q e. Pred ( R , ( A X. B ) , <. x , y >. ) ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) <-> ( q e. ( A X. B ) -> ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) ) )
29 elin 
 |-  ( q e. ( ( A X. B ) i^i Pred ( R , ( A X. B ) , <. x , y >. ) ) <-> ( q e. ( A X. B ) /\ q e. Pred ( R , ( A X. B ) , <. x , y >. ) ) )
30 predss 
 |-  Pred ( R , ( A X. B ) , <. x , y >. ) C_ ( A X. B )
31 sseqin2 
 |-  ( Pred ( R , ( A X. B ) , <. x , y >. ) C_ ( A X. B ) <-> ( ( A X. B ) i^i Pred ( R , ( A X. B ) , <. x , y >. ) ) = Pred ( R , ( A X. B ) , <. x , y >. ) )
32 30 31 mpbi 
 |-  ( ( A X. B ) i^i Pred ( R , ( A X. B ) , <. x , y >. ) ) = Pred ( R , ( A X. B ) , <. x , y >. )
33 32 eleq2i 
 |-  ( q e. ( ( A X. B ) i^i Pred ( R , ( A X. B ) , <. x , y >. ) ) <-> q e. Pred ( R , ( A X. B ) , <. x , y >. ) )
34 29 33 bitr3i 
 |-  ( ( q e. ( A X. B ) /\ q e. Pred ( R , ( A X. B ) , <. x , y >. ) ) <-> q e. Pred ( R , ( A X. B ) , <. x , y >. ) )
35 34 imbi1i 
 |-  ( ( ( q e. ( A X. B ) /\ q e. Pred ( R , ( A X. B ) , <. x , y >. ) ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) <-> ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) )
36 28 35 bitr3i 
 |-  ( ( q e. ( A X. B ) -> ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) ) <-> ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) )
37 36 albii 
 |-  ( A. q ( q e. ( A X. B ) -> ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) ) <-> A. q ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) )
38 df-ral 
 |-  ( A. q e. ( A X. B ) ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) <-> A. q ( q e. ( A X. B ) -> ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) ) )
39 df-ral 
 |-  ( A. q e. Pred ( R , ( A X. B ) , <. x , y >. ) [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch <-> A. q ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) )
40 37 38 39 3bitr4ri 
 |-  ( A. q e. Pred ( R , ( A X. B ) , <. x , y >. ) [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch <-> A. q e. ( A X. B ) ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) )
41 nfv 
 |-  F/ z q e. Pred ( R , ( A X. B ) , <. x , y >. )
42 nfsbc1v 
 |-  F/ z [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch
43 41 42 nfim 
 |-  F/ z ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch )
44 nfv 
 |-  F/ w q e. Pred ( R , ( A X. B ) , <. x , y >. )
45 nfcv 
 |-  F/_ w ( 1st ` q )
46 nfsbc1v 
 |-  F/ w [. ( 2nd ` q ) / w ]. ch
47 45 46 nfsbcw 
 |-  F/ w [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch
48 44 47 nfim 
 |-  F/ w ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch )
49 nfv 
 |-  F/ q ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch )
50 eleq1 
 |-  ( q = <. z , w >. -> ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) <-> <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) ) )
51 sbcopeq1a 
 |-  ( q = <. z , w >. -> ( [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch <-> ch ) )
52 50 51 imbi12d 
 |-  ( q = <. z , w >. -> ( ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) <-> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) ) )
53 43 48 49 52 ralxpf 
 |-  ( A. q e. ( A X. B ) ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) <-> A. z e. A A. w e. B ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) )
54 r2al 
 |-  ( A. z e. A A. w e. B ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) <-> A. z A. w ( ( z e. A /\ w e. B ) -> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) ) )
55 impexp 
 |-  ( ( ( <. z , w >. e. ( A X. B ) /\ <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) ) -> ch ) <-> ( <. z , w >. e. ( A X. B ) -> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) ) )
56 opelxp 
 |-  ( <. z , w >. e. ( A X. B ) <-> ( z e. A /\ w e. B ) )
57 56 imbi1i 
 |-  ( ( <. z , w >. e. ( A X. B ) -> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) ) <-> ( ( z e. A /\ w e. B ) -> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) ) )
58 55 57 bitri 
 |-  ( ( ( <. z , w >. e. ( A X. B ) /\ <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) ) -> ch ) <-> ( ( z e. A /\ w e. B ) -> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) ) )
59 elin 
 |-  ( <. z , w >. e. ( ( A X. B ) i^i Pred ( R , ( A X. B ) , <. x , y >. ) ) <-> ( <. z , w >. e. ( A X. B ) /\ <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) ) )
60 32 eleq2i 
 |-  ( <. z , w >. e. ( ( A X. B ) i^i Pred ( R , ( A X. B ) , <. x , y >. ) ) <-> <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) )
61 59 60 bitr3i 
 |-  ( ( <. z , w >. e. ( A X. B ) /\ <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) ) <-> <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) )
62 61 imbi1i 
 |-  ( ( ( <. z , w >. e. ( A X. B ) /\ <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) ) -> ch ) <-> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) )
63 58 62 bitr3i 
 |-  ( ( ( z e. A /\ w e. B ) -> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) ) <-> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) )
64 63 2albii 
 |-  ( A. z A. w ( ( z e. A /\ w e. B ) -> ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) ) <-> A. z A. w ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) )
65 53 54 64 3bitri 
 |-  ( A. q e. ( A X. B ) ( q e. Pred ( R , ( A X. B ) , <. x , y >. ) -> [. ( 1st ` q ) / z ]. [. ( 2nd ` q ) / w ]. ch ) <-> A. z A. w ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) )
66 27 40 65 3bitri 
 |-  ( A. q e. Pred ( R , ( A X. B ) , <. x , y >. ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph <-> A. z A. w ( <. z , w >. e. Pred ( R , ( A X. B ) , <. x , y >. ) -> ch ) )
67 66 1 biimtrid 
 |-  ( ( x e. A /\ y e. B ) -> ( A. q e. Pred ( R , ( A X. B ) , <. x , y >. ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> ph ) )
68 predeq3 
 |-  ( p = <. x , y >. -> Pred ( R , ( A X. B ) , p ) = Pred ( R , ( A X. B ) , <. x , y >. ) )
69 68 raleqdv 
 |-  ( p = <. x , y >. -> ( A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph <-> A. q e. Pred ( R , ( A X. B ) , <. x , y >. ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph ) )
70 sbcopeq1a 
 |-  ( p = <. x , y >. -> ( [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph <-> ph ) )
71 69 70 imbi12d 
 |-  ( p = <. x , y >. -> ( ( A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph ) <-> ( A. q e. Pred ( R , ( A X. B ) , <. x , y >. ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> ph ) ) )
72 67 71 syl5ibrcom 
 |-  ( ( x e. A /\ y e. B ) -> ( p = <. x , y >. -> ( A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph ) ) )
73 72 ex 
 |-  ( x e. A -> ( y e. B -> ( p = <. x , y >. -> ( A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph ) ) ) )
74 12 21 73 rexlimd 
 |-  ( x e. A -> ( E. y e. B p = <. x , y >. -> ( A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph ) ) )
75 11 74 rexlimi 
 |-  ( E. x e. A E. y e. B p = <. x , y >. -> ( A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph ) )
76 6 75 sylbi 
 |-  ( p e. ( A X. B ) -> ( A. q e. Pred ( R , ( A X. B ) , p ) [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph -> [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph ) )
77 fveq2 
 |-  ( p = q -> ( 1st ` p ) = ( 1st ` q ) )
78 fveq2 
 |-  ( p = q -> ( 2nd ` p ) = ( 2nd ` q ) )
79 78 sbceq1d 
 |-  ( p = q -> ( [. ( 2nd ` p ) / y ]. ph <-> [. ( 2nd ` q ) / y ]. ph ) )
80 77 79 sbceqbid 
 |-  ( p = q -> ( [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph <-> [. ( 1st ` q ) / x ]. [. ( 2nd ` q ) / y ]. ph ) )
81 76 80 frpoins2g 
 |-  ( ( R Fr ( A X. B ) /\ R Po ( A X. B ) /\ R Se ( A X. B ) ) -> A. p e. ( A X. B ) [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph )
82 ralxpes 
 |-  ( A. p e. ( A X. B ) [. ( 1st ` p ) / x ]. [. ( 2nd ` p ) / y ]. ph <-> A. x e. A A. y e. B ph )
83 81 82 sylib 
 |-  ( ( R Fr ( A X. B ) /\ R Po ( A X. B ) /\ R Se ( A X. B ) ) -> A. x e. A A. y e. B ph )
84 4 5 rspc2va 
 |-  ( ( ( X e. A /\ Y e. B ) /\ A. x e. A A. y e. B ph ) -> ta )
85 83 84 sylan2 
 |-  ( ( ( X e. A /\ Y e. B ) /\ ( R Fr ( A X. B ) /\ R Po ( A X. B ) /\ R Se ( A X. B ) ) ) -> ta )
86 85 ancoms 
 |-  ( ( ( R Fr ( A X. B ) /\ R Po ( A X. B ) /\ R Se ( A X. B ) ) /\ ( X e. A /\ Y e. B ) ) -> ta )