Metamath Proof Explorer

Theorem xpord2ind

Description: Induction over the cross product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 22-Aug-2024)

Ref Expression
Hypotheses xpord2.1 ⊢ T = x y | x ∈ A × B ∧ y ∈ A × B ∧ 1 st ⁡ x R 1 st ⁡ y ∨ 1 st ⁡ x = 1 st ⁡ y ∧ 2 nd ⁡ x S 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y
xpord2ind.1 ⊢ R Fr A
xpord2ind.2 ⊢ R Po A
xpord2ind.3 ⊢ R Se A
xpord2ind.4 ⊢ S Fr B
xpord2ind.5 ⊢ S Po B
xpord2ind.6 ⊢ S Se B
xpord2ind.7 ⊢ a = c → φ ↔ ψ
xpord2ind.8 ⊢ b = d → ψ ↔ χ
xpord2ind.9 ⊢ a = c → θ ↔ χ
xpord2ind.11 ⊢ a = X → φ ↔ τ
xpord2ind.12 ⊢ b = Y → τ ↔ η
xpord2ind.i ⊢ a ∈ A ∧ b ∈ B → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b χ ∧ ∀ c ∈ Pred R A a ψ ∧ ∀ d ∈ Pred S B b θ → φ
Assertion xpord2ind ⊢ X ∈ A ∧ Y ∈ B → η

Proof

Step Hyp Ref Expression
1 xpord2.1 ⊢ T = x y | x ∈ A × B ∧ y ∈ A × B ∧ 1 st ⁡ x R 1 st ⁡ y ∨ 1 st ⁡ x = 1 st ⁡ y ∧ 2 nd ⁡ x S 2 nd ⁡ y ∨ 2 nd ⁡ x = 2 nd ⁡ y ∧ x ≠ y
2 xpord2ind.1 ⊢ R Fr A
3 xpord2ind.2 ⊢ R Po A
4 xpord2ind.3 ⊢ R Se A
5 xpord2ind.4 ⊢ S Fr B
6 xpord2ind.5 ⊢ S Po B
7 xpord2ind.6 ⊢ S Se B
8 xpord2ind.7 ⊢ a = c → φ ↔ ψ
9 xpord2ind.8 ⊢ b = d → ψ ↔ χ
10 xpord2ind.9 ⊢ a = c → θ ↔ χ
11 xpord2ind.11 ⊢ a = X → φ ↔ τ
12 xpord2ind.12 ⊢ b = Y → τ ↔ η
13 xpord2ind.i ⊢ a ∈ A ∧ b ∈ B → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b χ ∧ ∀ c ∈ Pred R A a ψ ∧ ∀ d ∈ Pred S B b θ → φ
14 2 a1i ⊢ ⊤ → R Fr A
15 5 a1i ⊢ ⊤ → S Fr B
16 1 14 15 frxp2 ⊢ ⊤ → T Fr A × B
17 3 a1i ⊢ ⊤ → R Po A
18 6 a1i ⊢ ⊤ → S Po B
19 1 17 18 poxp2 ⊢ ⊤ → T Po A × B
20 4 a1i ⊢ ⊤ → R Se A
21 7 a1i ⊢ ⊤ → S Se B
22 1 20 21 sexp2 ⊢ ⊤ → T Se A × B
23 16 19 22 3jca ⊢ ⊤ → T Fr A × B ∧ T Po A × B ∧ T Se A × B
24 23 mptru ⊢ T Fr A × B ∧ T Po A × B ∧ T Se A × B
25 1 xpord2pred ⊢ a ∈ A ∧ b ∈ B → Pred T A × B a b = Pred R A a ∪ a × Pred S B b ∪ b ∖ a b
26 25 eleq2d ⊢ a ∈ A ∧ b ∈ B → c d ∈ Pred T A × B a b ↔ c d ∈ Pred R A a ∪ a × Pred S B b ∪ b ∖ a b
27 26 imbi1d ⊢ a ∈ A ∧ b ∈ B → c d ∈ Pred T A × B a b → χ ↔ c d ∈ Pred R A a ∪ a × Pred S B b ∪ b ∖ a b → χ
28 eldif ⊢ c d ∈ Pred R A a ∪ a × Pred S B b ∪ b ∖ a b ↔ c d ∈ Pred R A a ∪ a × Pred S B b ∪ b ∧ ¬ c d ∈ a b
29 opelxp ⊢ c d ∈ Pred R A a ∪ a × Pred S B b ∪ b ↔ c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b
30 opex ⊢ c d ∈ V
31 30 elsn ⊢ c d ∈ a b ↔ c d = a b
32 31 notbii ⊢ ¬ c d ∈ a b ↔ ¬ c d = a b
33 df-ne ⊢ c d ≠ a b ↔ ¬ c d = a b
34 vex ⊢ c ∈ V
35 vex ⊢ d ∈ V
36 34 35 opthne ⊢ c d ≠ a b ↔ c ≠ a ∨ d ≠ b
37 32 33 36 3bitr2i ⊢ ¬ c d ∈ a b ↔ c ≠ a ∨ d ≠ b
38 29 37 anbi12i ⊢ c d ∈ Pred R A a ∪ a × Pred S B b ∪ b ∧ ¬ c d ∈ a b ↔ c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b ∧ c ≠ a ∨ d ≠ b
39 28 38 bitri ⊢ c d ∈ Pred R A a ∪ a × Pred S B b ∪ b ∖ a b ↔ c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b ∧ c ≠ a ∨ d ≠ b
40 39 imbi1i ⊢ c d ∈ Pred R A a ∪ a × Pred S B b ∪ b ∖ a b → χ ↔ c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b ∧ c ≠ a ∨ d ≠ b → χ
41 impexp ⊢ c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b ∧ c ≠ a ∨ d ≠ b → χ ↔ c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b → c ≠ a ∨ d ≠ b → χ
42 40 41 bitri ⊢ c d ∈ Pred R A a ∪ a × Pred S B b ∪ b ∖ a b → χ ↔ c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b → c ≠ a ∨ d ≠ b → χ
43 27 42 bitrdi ⊢ a ∈ A ∧ b ∈ B → c d ∈ Pred T A × B a b → χ ↔ c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b → c ≠ a ∨ d ≠ b → χ
44 43 2albidv ⊢ a ∈ A ∧ b ∈ B → ∀ c ∀ d c d ∈ Pred T A × B a b → χ ↔ ∀ c ∀ d c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b → c ≠ a ∨ d ≠ b → χ
45 r2al ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ ↔ ∀ c ∀ d c ∈ Pred R A a ∪ a ∧ d ∈ Pred S B b ∪ b → c ≠ a ∨ d ≠ b → χ
46 44 45 bitr4di ⊢ a ∈ A ∧ b ∈ B → ∀ c ∀ d c d ∈ Pred T A × B a b → χ ↔ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ
47 ssun1 ⊢ Pred R A a ⊆ Pred R A a ∪ a
48 ssralv ⊢ Pred R A a ⊆ Pred R A a ∪ a → ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ
49 47 48 ax-mp ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ
50 ssun1 ⊢ Pred S B b ⊆ Pred S B b ∪ b
51 ssralv ⊢ Pred S B b ⊆ Pred S B b ∪ b → ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ
52 50 51 ax-mp ⊢ ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ
53 52 ralimi ⊢ ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ
54 49 53 syl ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ
55 predpoirr ⊢ S Po B → ¬ b ∈ Pred S B b
56 6 55 ax-mp ⊢ ¬ b ∈ Pred S B b
57 eleq1w ⊢ d = b → d ∈ Pred S B b ↔ b ∈ Pred S B b
58 56 57 mtbiri ⊢ d = b → ¬ d ∈ Pred S B b
59 58 necon2ai ⊢ d ∈ Pred S B b → d ≠ b
60 59 olcd ⊢ d ∈ Pred S B b → c ≠ a ∨ d ≠ b
61 pm2.27 ⊢ c ≠ a ∨ d ≠ b → c ≠ a ∨ d ≠ b → χ → χ
62 60 61 syl ⊢ d ∈ Pred S B b → c ≠ a ∨ d ≠ b → χ → χ
63 62 ralimia ⊢ ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ → ∀ d ∈ Pred S B b χ
64 63 ralimi ⊢ ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b χ
65 54 64 syl ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b χ
66 ssun2 ⊢ b ⊆ Pred S B b ∪ b
67 ssralv ⊢ b ⊆ Pred S B b ∪ b → ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ d ∈ b c ≠ a ∨ d ≠ b → χ
68 66 67 ax-mp ⊢ ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ d ∈ b c ≠ a ∨ d ≠ b → χ
69 68 ralimi ⊢ ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ∀ d ∈ b c ≠ a ∨ d ≠ b → χ
70 49 69 syl ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ∀ d ∈ b c ≠ a ∨ d ≠ b → χ
71 vex ⊢ b ∈ V
72 neeq1 ⊢ d = b → d ≠ b ↔ b ≠ b
73 72 orbi2d ⊢ d = b → c ≠ a ∨ d ≠ b ↔ c ≠ a ∨ b ≠ b
74 9 equcoms ⊢ d = b → ψ ↔ χ
75 74 bicomd ⊢ d = b → χ ↔ ψ
76 73 75 imbi12d ⊢ d = b → c ≠ a ∨ d ≠ b → χ ↔ c ≠ a ∨ b ≠ b → ψ
77 71 76 ralsn ⊢ ∀ d ∈ b c ≠ a ∨ d ≠ b → χ ↔ c ≠ a ∨ b ≠ b → ψ
78 77 ralbii ⊢ ∀ c ∈ Pred R A a ∀ d ∈ b c ≠ a ∨ d ≠ b → χ ↔ ∀ c ∈ Pred R A a c ≠ a ∨ b ≠ b → ψ
79 70 78 sylib ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a c ≠ a ∨ b ≠ b → ψ
80 predpoirr ⊢ R Po A → ¬ a ∈ Pred R A a
81 3 80 ax-mp ⊢ ¬ a ∈ Pred R A a
82 eleq1w ⊢ c = a → c ∈ Pred R A a ↔ a ∈ Pred R A a
83 81 82 mtbiri ⊢ c = a → ¬ c ∈ Pred R A a
84 83 necon2ai ⊢ c ∈ Pred R A a → c ≠ a
85 84 orcd ⊢ c ∈ Pred R A a → c ≠ a ∨ b ≠ b
86 pm2.27 ⊢ c ≠ a ∨ b ≠ b → c ≠ a ∨ b ≠ b → ψ → ψ
87 85 86 syl ⊢ c ∈ Pred R A a → c ≠ a ∨ b ≠ b → ψ → ψ
88 87 ralimia ⊢ ∀ c ∈ Pred R A a c ≠ a ∨ b ≠ b → ψ → ∀ c ∈ Pred R A a ψ
89 79 88 syl ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ψ
90 ssun2 ⊢ a ⊆ Pred R A a ∪ a
91 ssralv ⊢ a ⊆ Pred R A a ∪ a → ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ
92 90 91 ax-mp ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ
93 52 ralimi ⊢ ∀ c ∈ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ a ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ
94 92 93 syl ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ a ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ
95 vex ⊢ a ∈ V
96 neeq1 ⊢ c = a → c ≠ a ↔ a ≠ a
97 96 orbi1d ⊢ c = a → c ≠ a ∨ d ≠ b ↔ a ≠ a ∨ d ≠ b
98 10 equcoms ⊢ c = a → θ ↔ χ
99 98 bicomd ⊢ c = a → χ ↔ θ
100 97 99 imbi12d ⊢ c = a → c ≠ a ∨ d ≠ b → χ ↔ a ≠ a ∨ d ≠ b → θ
101 100 ralbidv ⊢ c = a → ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ ↔ ∀ d ∈ Pred S B b a ≠ a ∨ d ≠ b → θ
102 95 101 ralsn ⊢ ∀ c ∈ a ∀ d ∈ Pred S B b c ≠ a ∨ d ≠ b → χ ↔ ∀ d ∈ Pred S B b a ≠ a ∨ d ≠ b → θ
103 94 102 sylib ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ d ∈ Pred S B b a ≠ a ∨ d ≠ b → θ
104 59 olcd ⊢ d ∈ Pred S B b → a ≠ a ∨ d ≠ b
105 pm2.27 ⊢ a ≠ a ∨ d ≠ b → a ≠ a ∨ d ≠ b → θ → θ
106 104 105 syl ⊢ d ∈ Pred S B b → a ≠ a ∨ d ≠ b → θ → θ
107 106 ralimia ⊢ ∀ d ∈ Pred S B b a ≠ a ∨ d ≠ b → θ → ∀ d ∈ Pred S B b θ
108 103 107 syl ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ d ∈ Pred S B b θ
109 65 89 108 3jca ⊢ ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → ∀ c ∈ Pred R A a ∀ d ∈ Pred S B b χ ∧ ∀ c ∈ Pred R A a ψ ∧ ∀ d ∈ Pred S B b θ
110 109 13 syl5 ⊢ a ∈ A ∧ b ∈ B → ∀ c ∈ Pred R A a ∪ a ∀ d ∈ Pred S B b ∪ b c ≠ a ∨ d ≠ b → χ → φ
111 46 110 sylbid ⊢ a ∈ A ∧ b ∈ B → ∀ c ∀ d c d ∈ Pred T A × B a b → χ → φ
112 111 8 9 11 12 frpoins3xpg ⊢ T Fr A × B ∧ T Po A × B ∧ T Se A × B ∧ X ∈ A ∧ Y ∈ B → η
113 24 112 mpan ⊢ X ∈ A ∧ Y ∈ B → η