Metamath Proof Explorer

Theorem xpord2indlem

Description: Induction over the Cartesian 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=xy|x∈A×B∧y∈A×B∧1st⁡xR1st⁡y∨1st⁡x=1st⁡y∧2nd⁡xS2nd⁡y∨2nd⁡x=2nd⁡y∧x≠y
xpord2indlem.1 ⊢RFrA
xpord2indlem.2 ⊢RPoA
xpord2indlem.3 ⊢RSeA
xpord2indlem.4 ⊢SFrB
xpord2indlem.5 ⊢SPoB
xpord2indlem.6 ⊢SSeB
xpord2indlem.7 ⊢a=c→φ↔ψ
xpord2indlem.8 ⊢b=d→ψ↔χ
xpord2indlem.9 ⊢a=c→θ↔χ
xpord2indlem.11 ⊢a=X→φ↔τ
xpord2indlem.12 ⊢b=Y→τ↔η
xpord2indlem.i ⊢a∈A∧b∈B→∀c∈PredRAa∀d∈PredSBbχ∧∀c∈PredRAaψ∧∀d∈PredSBbθ→φ
Assertion xpord2indlem ⊢X∈A∧Y∈B→η

Proof

Step Hyp Ref Expression
1 xpord2.1 ⊢T=xy|x∈A×B∧y∈A×B∧1st⁡xR1st⁡y∨1st⁡x=1st⁡y∧2nd⁡xS2nd⁡y∨2nd⁡x=2nd⁡y∧x≠y
2 xpord2indlem.1 ⊢RFrA
3 xpord2indlem.2 ⊢RPoA
4 xpord2indlem.3 ⊢RSeA
5 xpord2indlem.4 ⊢SFrB
6 xpord2indlem.5 ⊢SPoB
7 xpord2indlem.6 ⊢SSeB
8 xpord2indlem.7 ⊢a=c→φ↔ψ
9 xpord2indlem.8 ⊢b=d→ψ↔χ
10 xpord2indlem.9 ⊢a=c→θ↔χ
11 xpord2indlem.11 ⊢a=X→φ↔τ
12 xpord2indlem.12 ⊢b=Y→τ↔η
13 xpord2indlem.i ⊢a∈A∧b∈B→∀c∈PredRAa∀d∈PredSBbχ∧∀c∈PredRAaψ∧∀d∈PredSBbθ→φ
14 2 a1i ⊢⊤→RFrA
15 5 a1i ⊢⊤→SFrB
16 1 14 15 frxp2 ⊢⊤→TFrA×B
17 3 a1i ⊢⊤→RPoA
18 6 a1i ⊢⊤→SPoB
19 1 17 18 poxp2 ⊢⊤→TPoA×B
20 4 a1i ⊢⊤→RSeA
21 7 a1i ⊢⊤→SSeB
22 1 20 21 sexp2 ⊢⊤→TSeA×B
23 16 19 22 3jca ⊢⊤→TFrA×B∧TPoA×B∧TSeA×B
24 23 mptru ⊢TFrA×B∧TPoA×B∧TSeA×B
25 1 xpord2pred ⊢a∈A∧b∈B→PredTA×Bab=PredRAa∪a×PredSBb∪b∖ab
26 25 eleq2d ⊢a∈A∧b∈B→cd∈PredTA×Bab↔cd∈PredRAa∪a×PredSBb∪b∖ab
27 26 imbi1d ⊢a∈A∧b∈B→cd∈PredTA×Bab→χ↔cd∈PredRAa∪a×PredSBb∪b∖ab→χ
28 eldif ⊢cd∈PredRAa∪a×PredSBb∪b∖ab↔cd∈PredRAa∪a×PredSBb∪b∧¬cd∈ab
29 opelxp ⊢cd∈PredRAa∪a×PredSBb∪b↔c∈PredRAa∪a∧d∈PredSBb∪b
30 opex ⊢cd∈V
31 30 elsn ⊢cd∈ab↔cd=ab
32 31 notbii ⊢¬cd∈ab↔¬cd=ab
33 df-ne ⊢cd≠ab↔¬cd=ab
34 vex ⊢c∈V
35 vex ⊢d∈V
36 34 35 opthne ⊢cd≠ab↔c≠a∨d≠b
37 32 33 36 3bitr2i ⊢¬cd∈ab↔c≠a∨d≠b
38 29 37 anbi12i ⊢cd∈PredRAa∪a×PredSBb∪b∧¬cd∈ab↔c∈PredRAa∪a∧d∈PredSBb∪b∧c≠a∨d≠b
39 28 38 bitri ⊢cd∈PredRAa∪a×PredSBb∪b∖ab↔c∈PredRAa∪a∧d∈PredSBb∪b∧c≠a∨d≠b
40 39 imbi1i ⊢cd∈PredRAa∪a×PredSBb∪b∖ab→χ↔c∈PredRAa∪a∧d∈PredSBb∪b∧c≠a∨d≠b→χ
41 impexp ⊢c∈PredRAa∪a∧d∈PredSBb∪b∧c≠a∨d≠b→χ↔c∈PredRAa∪a∧d∈PredSBb∪b→c≠a∨d≠b→χ
42 40 41 bitri ⊢cd∈PredRAa∪a×PredSBb∪b∖ab→χ↔c∈PredRAa∪a∧d∈PredSBb∪b→c≠a∨d≠b→χ
43 27 42 bitrdi ⊢a∈A∧b∈B→cd∈PredTA×Bab→χ↔c∈PredRAa∪a∧d∈PredSBb∪b→c≠a∨d≠b→χ
44 43 2albidv ⊢a∈A∧b∈B→∀c∀dcd∈PredTA×Bab→χ↔∀c∀dc∈PredRAa∪a∧d∈PredSBb∪b→c≠a∨d≠b→χ
45 r2al ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ↔∀c∀dc∈PredRAa∪a∧d∈PredSBb∪b→c≠a∨d≠b→χ
46 44 45 bitr4di ⊢a∈A∧b∈B→∀c∀dcd∈PredTA×Bab→χ↔∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ
47 ssun1 ⊢PredRAa⊆PredRAa∪a
48 ssralv ⊢PredRAa⊆PredRAa∪a→∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAa∀d∈PredSBb∪bc≠a∨d≠b→χ
49 47 48 ax-mp ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAa∀d∈PredSBb∪bc≠a∨d≠b→χ
50 ssun1 ⊢PredSBb⊆PredSBb∪b
51 ssralv ⊢PredSBb⊆PredSBb∪b→∀d∈PredSBb∪bc≠a∨d≠b→χ→∀d∈PredSBbc≠a∨d≠b→χ
52 50 51 ax-mp ⊢∀d∈PredSBb∪bc≠a∨d≠b→χ→∀d∈PredSBbc≠a∨d≠b→χ
53 52 ralimi ⊢∀c∈PredRAa∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAa∀d∈PredSBbc≠a∨d≠b→χ
54 49 53 syl ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAa∀d∈PredSBbc≠a∨d≠b→χ
55 predpoirr ⊢SPoB→¬b∈PredSBb
56 6 55 ax-mp ⊢¬b∈PredSBb
57 eleq1w ⊢d=b→d∈PredSBb↔b∈PredSBb
58 56 57 mtbiri ⊢d=b→¬d∈PredSBb
59 58 necon2ai ⊢d∈PredSBb→d≠b
60 59 olcd ⊢d∈PredSBb→c≠a∨d≠b
61 pm2.27 ⊢c≠a∨d≠b→c≠a∨d≠b→χ→χ
62 60 61 syl ⊢d∈PredSBb→c≠a∨d≠b→χ→χ
63 62 ralimia ⊢∀d∈PredSBbc≠a∨d≠b→χ→∀d∈PredSBbχ
64 63 ralimi ⊢∀c∈PredRAa∀d∈PredSBbc≠a∨d≠b→χ→∀c∈PredRAa∀d∈PredSBbχ
65 54 64 syl ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAa∀d∈PredSBbχ
66 ssun2 ⊢b⊆PredSBb∪b
67 ssralv ⊢b⊆PredSBb∪b→∀d∈PredSBb∪bc≠a∨d≠b→χ→∀d∈bc≠a∨d≠b→χ
68 66 67 ax-mp ⊢∀d∈PredSBb∪bc≠a∨d≠b→χ→∀d∈bc≠a∨d≠b→χ
69 68 ralimi ⊢∀c∈PredRAa∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAa∀d∈bc≠a∨d≠b→χ
70 49 69 syl ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAa∀d∈bc≠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∈bc≠a∨d≠b→χ↔c≠a∨b≠b→ψ
78 77 ralbii ⊢∀c∈PredRAa∀d∈bc≠a∨d≠b→χ↔∀c∈PredRAac≠a∨b≠b→ψ
79 70 78 sylib ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAac≠a∨b≠b→ψ
80 predpoirr ⊢RPoA→¬a∈PredRAa
81 3 80 ax-mp ⊢¬a∈PredRAa
82 eleq1w ⊢c=a→c∈PredRAa↔a∈PredRAa
83 81 82 mtbiri ⊢c=a→¬c∈PredRAa
84 83 necon2ai ⊢c∈PredRAa→c≠a
85 84 orcd ⊢c∈PredRAa→c≠a∨b≠b
86 pm2.27 ⊢c≠a∨b≠b→c≠a∨b≠b→ψ→ψ
87 85 86 syl ⊢c∈PredRAa→c≠a∨b≠b→ψ→ψ
88 87 ralimia ⊢∀c∈PredRAac≠a∨b≠b→ψ→∀c∈PredRAaψ
89 79 88 syl ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAaψ
90 ssun2 ⊢a⊆PredRAa∪a
91 ssralv ⊢a⊆PredRAa∪a→∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈a∀d∈PredSBb∪bc≠a∨d≠b→χ
92 90 91 ax-mp ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈a∀d∈PredSBb∪bc≠a∨d≠b→χ
93 52 ralimi ⊢∀c∈a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈a∀d∈PredSBbc≠a∨d≠b→χ
94 92 93 syl ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈a∀d∈PredSBbc≠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∈PredSBbc≠a∨d≠b→χ↔∀d∈PredSBba≠a∨d≠b→θ
102 95 101 ralsn ⊢∀c∈a∀d∈PredSBbc≠a∨d≠b→χ↔∀d∈PredSBba≠a∨d≠b→θ
103 94 102 sylib ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀d∈PredSBba≠a∨d≠b→θ
104 59 olcd ⊢d∈PredSBb→a≠a∨d≠b
105 pm2.27 ⊢a≠a∨d≠b→a≠a∨d≠b→θ→θ
106 104 105 syl ⊢d∈PredSBb→a≠a∨d≠b→θ→θ
107 106 ralimia ⊢∀d∈PredSBba≠a∨d≠b→θ→∀d∈PredSBbθ
108 103 107 syl ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀d∈PredSBbθ
109 65 89 108 3jca ⊢∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→∀c∈PredRAa∀d∈PredSBbχ∧∀c∈PredRAaψ∧∀d∈PredSBbθ
110 109 13 syl5 ⊢a∈A∧b∈B→∀c∈PredRAa∪a∀d∈PredSBb∪bc≠a∨d≠b→χ→φ
111 46 110 sylbid ⊢a∈A∧b∈B→∀c∀dcd∈PredTA×Bab→χ→φ
112 111 8 9 11 12 frpoins3xpg ⊢TFrA×B∧TPoA×B∧TSeA×B∧X∈A∧Y∈B→η
113 24 112 mpan ⊢X∈A∧Y∈B→η