Metamath Proof Explorer


Theorem frpoins3xpg

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

Ref Expression
Hypotheses frpoins3xpg.1 x A y B z w z w Pred R A × B x y χ φ
frpoins3xpg.2 x = z φ ψ
frpoins3xpg.3 y = w ψ χ
frpoins3xpg.4 x = X φ θ
frpoins3xpg.5 y = Y θ τ
Assertion frpoins3xpg R Fr A × B R Po A × B R Se A × B X A Y B τ

Proof

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