Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xpord2ind Structured version   Visualization version   GIF version

Theorem xpord2ind 33405
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.)
Hypotheses
Ref Expression
xpord2.1 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st𝑥)𝑅(1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥)𝑆(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}
xpord2ind.1 𝑅 Fr 𝐴
xpord2ind.2 𝑅 Po 𝐴
xpord2ind.3 𝑅 Se 𝐴
xpord2ind.4 𝑆 Fr 𝐵
xpord2ind.5 𝑆 Po 𝐵
xpord2ind.6 𝑆 Se 𝐵
xpord2ind.7 (𝑎 = 𝑐 → (𝜑𝜓))
xpord2ind.8 (𝑏 = 𝑑 → (𝜓𝜒))
xpord2ind.9 (𝑎 = 𝑐 → (𝜃𝜒))
xpord2ind.11 (𝑎 = 𝑋 → (𝜑𝜏))
xpord2ind.12 (𝑏 = 𝑌 → (𝜏𝜂))
xpord2ind.i ((𝑎𝐴𝑏𝐵) → ((∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃) → 𝜑))
Assertion
Ref Expression
xpord2ind ((𝑋𝐴𝑌𝐵) → 𝜂)
Distinct variable groups:   𝐴,𝑎,𝑏,𝑐,𝑑   𝜓,𝑎   𝜏,𝑎   𝑥,𝐴,𝑦   𝐵,𝑎,𝑏,𝑐   𝜒,𝑏   𝑏,𝑑,𝐵   𝜂,𝑏   𝑥,𝐵,𝑦   𝑐,𝑑   𝜑,𝑐   𝜃,𝑐   𝜓,𝑑   𝑅,𝑐,𝑑   𝑥,𝑅,𝑦   𝑆,𝑐,𝑑   𝑥,𝑆,𝑦   𝑇,𝑎,𝑏,𝑐,𝑑   𝑋,𝑎,𝑏   𝑥,𝑦   𝑌,𝑏
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑎,𝑏,𝑑)   𝜓(𝑥,𝑦,𝑏,𝑐)   𝜒(𝑥,𝑦,𝑎,𝑐,𝑑)   𝜃(𝑥,𝑦,𝑎,𝑏,𝑑)   𝜏(𝑥,𝑦,𝑏,𝑐,𝑑)   𝜂(𝑥,𝑦,𝑎,𝑐,𝑑)   𝑅(𝑎,𝑏)   𝑆(𝑎,𝑏)   𝑇(𝑥,𝑦)   𝑋(𝑥,𝑦,𝑐,𝑑)   𝑌(𝑥,𝑦,𝑎,𝑐,𝑑)

Proof of Theorem xpord2ind
StepHypRef Expression
1 xpord2.1 . . . . 5 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st𝑥)𝑅(1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥)𝑆(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}
2 xpord2ind.1 . . . . . 6 𝑅 Fr 𝐴
32a1i 11 . . . . 5 (⊤ → 𝑅 Fr 𝐴)
4 xpord2ind.4 . . . . . 6 𝑆 Fr 𝐵
54a1i 11 . . . . 5 (⊤ → 𝑆 Fr 𝐵)
61, 3, 5frxp2 33402 . . . 4 (⊤ → 𝑇 Fr (𝐴 × 𝐵))
7 xpord2ind.2 . . . . . 6 𝑅 Po 𝐴
87a1i 11 . . . . 5 (⊤ → 𝑅 Po 𝐴)
9 xpord2ind.5 . . . . . 6 𝑆 Po 𝐵
109a1i 11 . . . . 5 (⊤ → 𝑆 Po 𝐵)
111, 8, 10poxp2 33401 . . . 4 (⊤ → 𝑇 Po (𝐴 × 𝐵))
12 xpord2ind.3 . . . . . 6 𝑅 Se 𝐴
1312a1i 11 . . . . 5 (⊤ → 𝑅 Se 𝐴)
14 xpord2ind.6 . . . . . 6 𝑆 Se 𝐵
1514a1i 11 . . . . 5 (⊤ → 𝑆 Se 𝐵)
161, 13, 15sexp2 33404 . . . 4 (⊤ → 𝑇 Se (𝐴 × 𝐵))
176, 11, 163jca 1129 . . 3 (⊤ → (𝑇 Fr (𝐴 × 𝐵) ∧ 𝑇 Po (𝐴 × 𝐵) ∧ 𝑇 Se (𝐴 × 𝐵)))
1817mptru 1549 . 2 (𝑇 Fr (𝐴 × 𝐵) ∧ 𝑇 Po (𝐴 × 𝐵) ∧ 𝑇 Se (𝐴 × 𝐵))
191xpord2pred 33403 . . . . . . . . 9 ((𝑎𝐴𝑏𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))
2019eleq2d 2818 . . . . . . . 8 ((𝑎𝐴𝑏𝐵) → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
2120imbi1d 345 . . . . . . 7 ((𝑎𝐴𝑏𝐵) → ((⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝜒) ↔ (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝜒)))
22 eldif 3853 . . . . . . . . . 10 (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}))
23 opelxp 5561 . . . . . . . . . . 11 (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
24 opex 5322 . . . . . . . . . . . . . 14 𝑐, 𝑑⟩ ∈ V
2524elsn 4531 . . . . . . . . . . . . 13 (⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
2625notbii 323 . . . . . . . . . . . 12 (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
27 df-ne 2935 . . . . . . . . . . . 12 (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
28 vex 3402 . . . . . . . . . . . . 13 𝑐 ∈ V
29 vex 3402 . . . . . . . . . . . . 13 𝑑 ∈ V
3028, 29opthne 5340 . . . . . . . . . . . 12 (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ (𝑐𝑎𝑑𝑏))
3126, 27, 303bitr2i 302 . . . . . . . . . . 11 (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ (𝑐𝑎𝑑𝑏))
3223, 31anbi12i 630 . . . . . . . . . 10 ((⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ (𝑐𝑎𝑑𝑏)))
3322, 32bitri 278 . . . . . . . . 9 (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ (𝑐𝑎𝑑𝑏)))
3433imbi1i 353 . . . . . . . 8 ((⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝜒) ↔ (((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ (𝑐𝑎𝑑𝑏)) → 𝜒))
35 impexp 454 . . . . . . . 8 ((((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ (𝑐𝑎𝑑𝑏)) → 𝜒) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐𝑎𝑑𝑏) → 𝜒)))
3634, 35bitri 278 . . . . . . 7 ((⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝜒) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐𝑎𝑑𝑏) → 𝜒)))
3721, 36bitrdi 290 . . . . . 6 ((𝑎𝐴𝑏𝐵) → ((⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝜒) ↔ ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐𝑎𝑑𝑏) → 𝜒))))
38372albidv 1930 . . . . 5 ((𝑎𝐴𝑏𝐵) → (∀𝑐𝑑(⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝜒) ↔ ∀𝑐𝑑((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐𝑎𝑑𝑏) → 𝜒))))
39 r2al 3113 . . . . 5 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) ↔ ∀𝑐𝑑((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → ((𝑐𝑎𝑑𝑏) → 𝜒)))
4038, 39bitr4di 292 . . . 4 ((𝑎𝐴𝑏𝐵) → (∀𝑐𝑑(⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝜒) ↔ ∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒)))
41 ssun1 4062 . . . . . . . . 9 Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
42 ssralv 3943 . . . . . . . . 9 (Pred(𝑅, 𝐴, 𝑎) ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒)))
4341, 42ax-mp 5 . . . . . . . 8 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒))
44 ssun1 4062 . . . . . . . . . 10 Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
45 ssralv 3943 . . . . . . . . . 10 (Pred(𝑆, 𝐵, 𝑏) ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒)))
4644, 45ax-mp 5 . . . . . . . . 9 (∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒))
4746ralimi 3075 . . . . . . . 8 (∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒))
4843, 47syl 17 . . . . . . 7 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒))
49 predpoirr 6157 . . . . . . . . . . . . . 14 (𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏))
509, 49ax-mp 5 . . . . . . . . . . . . 13 ¬ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)
51 eleq1w 2815 . . . . . . . . . . . . 13 (𝑑 = 𝑏 → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ 𝑏 ∈ Pred(𝑆, 𝐵, 𝑏)))
5250, 51mtbiri 330 . . . . . . . . . . . 12 (𝑑 = 𝑏 → ¬ 𝑑 ∈ Pred(𝑆, 𝐵, 𝑏))
5352necon2ai 2963 . . . . . . . . . . 11 (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → 𝑑𝑏)
5453olcd 873 . . . . . . . . . 10 (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → (𝑐𝑎𝑑𝑏))
55 pm2.27 42 . . . . . . . . . 10 ((𝑐𝑎𝑑𝑏) → (((𝑐𝑎𝑑𝑏) → 𝜒) → 𝜒))
5654, 55syl 17 . . . . . . . . 9 (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → (((𝑐𝑎𝑑𝑏) → 𝜒) → 𝜒))
5756ralimia 3073 . . . . . . . 8 (∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
5857ralimi 3075 . . . . . . 7 (∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
5948, 58syl 17 . . . . . 6 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒)
60 ssun2 4063 . . . . . . . . . . 11 {𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})
61 ssralv 3943 . . . . . . . . . . 11 ({𝑏} ⊆ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) → (∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑑 ∈ {𝑏} ((𝑐𝑎𝑑𝑏) → 𝜒)))
6260, 61ax-mp 5 . . . . . . . . . 10 (∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑑 ∈ {𝑏} ((𝑐𝑎𝑑𝑏) → 𝜒))
6362ralimi 3075 . . . . . . . . 9 (∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ {𝑏} ((𝑐𝑎𝑑𝑏) → 𝜒))
6443, 63syl 17 . . . . . . . 8 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ {𝑏} ((𝑐𝑎𝑑𝑏) → 𝜒))
65 vex 3402 . . . . . . . . . 10 𝑏 ∈ V
66 neeq1 2996 . . . . . . . . . . . 12 (𝑑 = 𝑏 → (𝑑𝑏𝑏𝑏))
6766orbi2d 915 . . . . . . . . . . 11 (𝑑 = 𝑏 → ((𝑐𝑎𝑑𝑏) ↔ (𝑐𝑎𝑏𝑏)))
68 xpord2ind.8 . . . . . . . . . . . . 13 (𝑏 = 𝑑 → (𝜓𝜒))
6968equcoms 2032 . . . . . . . . . . . 12 (𝑑 = 𝑏 → (𝜓𝜒))
7069bicomd 226 . . . . . . . . . . 11 (𝑑 = 𝑏 → (𝜒𝜓))
7167, 70imbi12d 348 . . . . . . . . . 10 (𝑑 = 𝑏 → (((𝑐𝑎𝑑𝑏) → 𝜒) ↔ ((𝑐𝑎𝑏𝑏) → 𝜓)))
7265, 71ralsn 4572 . . . . . . . . 9 (∀𝑑 ∈ {𝑏} ((𝑐𝑎𝑑𝑏) → 𝜒) ↔ ((𝑐𝑎𝑏𝑏) → 𝜓))
7372ralbii 3080 . . . . . . . 8 (∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ {𝑏} ((𝑐𝑎𝑑𝑏) → 𝜒) ↔ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑐𝑎𝑏𝑏) → 𝜓))
7464, 73sylib 221 . . . . . . 7 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑐𝑎𝑏𝑏) → 𝜓))
75 predpoirr 6157 . . . . . . . . . . . . 13 (𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎))
767, 75ax-mp 5 . . . . . . . . . . . 12 ¬ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)
77 eleq1w 2815 . . . . . . . . . . . 12 (𝑐 = 𝑎 → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ 𝑎 ∈ Pred(𝑅, 𝐴, 𝑎)))
7876, 77mtbiri 330 . . . . . . . . . . 11 (𝑐 = 𝑎 → ¬ 𝑐 ∈ Pred(𝑅, 𝐴, 𝑎))
7978necon2ai 2963 . . . . . . . . . 10 (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) → 𝑐𝑎)
8079orcd 872 . . . . . . . . 9 (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) → (𝑐𝑎𝑏𝑏))
81 pm2.27 42 . . . . . . . . 9 ((𝑐𝑎𝑏𝑏) → (((𝑐𝑎𝑏𝑏) → 𝜓) → 𝜓))
8280, 81syl 17 . . . . . . . 8 (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) → (((𝑐𝑎𝑏𝑏) → 𝜓) → 𝜓))
8382ralimia 3073 . . . . . . 7 (∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)((𝑐𝑎𝑏𝑏) → 𝜓) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)
8474, 83syl 17 . . . . . 6 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓)
85 ssun2 4063 . . . . . . . . . 10 {𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})
86 ssralv 3943 . . . . . . . . . 10 ({𝑎} ⊆ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) → (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ {𝑎}∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒)))
8785, 86ax-mp 5 . . . . . . . . 9 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ {𝑎}∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒))
8846ralimi 3075 . . . . . . . . 9 (∀𝑐 ∈ {𝑎}∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ {𝑎}∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒))
8987, 88syl 17 . . . . . . . 8 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑐 ∈ {𝑎}∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒))
90 vex 3402 . . . . . . . . 9 𝑎 ∈ V
91 neeq1 2996 . . . . . . . . . . . 12 (𝑐 = 𝑎 → (𝑐𝑎𝑎𝑎))
9291orbi1d 916 . . . . . . . . . . 11 (𝑐 = 𝑎 → ((𝑐𝑎𝑑𝑏) ↔ (𝑎𝑎𝑑𝑏)))
93 xpord2ind.9 . . . . . . . . . . . . 13 (𝑎 = 𝑐 → (𝜃𝜒))
9493equcoms 2032 . . . . . . . . . . . 12 (𝑐 = 𝑎 → (𝜃𝜒))
9594bicomd 226 . . . . . . . . . . 11 (𝑐 = 𝑎 → (𝜒𝜃))
9692, 95imbi12d 348 . . . . . . . . . 10 (𝑐 = 𝑎 → (((𝑐𝑎𝑑𝑏) → 𝜒) ↔ ((𝑎𝑎𝑑𝑏) → 𝜃)))
9796ralbidv 3109 . . . . . . . . 9 (𝑐 = 𝑎 → (∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒) ↔ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑑𝑏) → 𝜃)))
9890, 97ralsn 4572 . . . . . . . 8 (∀𝑐 ∈ {𝑎}∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑐𝑎𝑑𝑏) → 𝜒) ↔ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑑𝑏) → 𝜃))
9989, 98sylib 221 . . . . . . 7 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑑𝑏) → 𝜃))
10053olcd 873 . . . . . . . . 9 (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → (𝑎𝑎𝑑𝑏))
101 pm2.27 42 . . . . . . . . 9 ((𝑎𝑎𝑑𝑏) → (((𝑎𝑎𝑑𝑏) → 𝜃) → 𝜃))
102100, 101syl 17 . . . . . . . 8 (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) → (((𝑎𝑎𝑑𝑏) → 𝜃) → 𝜃))
103102ralimia 3073 . . . . . . 7 (∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)((𝑎𝑎𝑑𝑏) → 𝜃) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃)
10499, 103syl 17 . . . . . 6 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃)
10559, 84, 1043jca 1129 . . . . 5 (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → (∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃))
106 xpord2ind.i . . . . 5 ((𝑎𝐴𝑏𝐵) → ((∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜒 ∧ ∀𝑐 ∈ Pred (𝑅, 𝐴, 𝑎)𝜓 ∧ ∀𝑑 ∈ Pred (𝑆, 𝐵, 𝑏)𝜃) → 𝜑))
107105, 106syl5 34 . . . 4 ((𝑎𝐴𝑏𝐵) → (∀𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎})∀𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})((𝑐𝑎𝑑𝑏) → 𝜒) → 𝜑))
10840, 107sylbid 243 . . 3 ((𝑎𝐴𝑏𝐵) → (∀𝑐𝑑(⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝜒) → 𝜑))
109 xpord2ind.7 . . 3 (𝑎 = 𝑐 → (𝜑𝜓))
110 xpord2ind.11 . . 3 (𝑎 = 𝑋 → (𝜑𝜏))
111 xpord2ind.12 . . 3 (𝑏 = 𝑌 → (𝜏𝜂))
112108, 109, 68, 110, 111frpoins3xpg 33388 . 2 (((𝑇 Fr (𝐴 × 𝐵) ∧ 𝑇 Po (𝐴 × 𝐵) ∧ 𝑇 Se (𝐴 × 𝐵)) ∧ (𝑋𝐴𝑌𝐵)) → 𝜂)
11318, 112mpan 690 1 ((𝑋𝐴𝑌𝐵) → 𝜂)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846  w3a 1088  wal 1540   = wceq 1542  wtru 1543  wcel 2114  wne 2934  wral 3053  cdif 3840  cun 3841  wss 3843  {csn 4516  cop 4522   class class class wbr 5030  {copab 5092   Po wpo 5440   Fr wfr 5480   Se wse 5481   × cxp 5523  Predcpred 6128  cfv 6339  1st c1st 7712  2nd c2nd 7713
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2710  ax-sep 5167  ax-nul 5174  ax-pow 5232  ax-pr 5296  ax-un 7479
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2540  df-eu 2570  df-clab 2717  df-cleq 2730  df-clel 2811  df-nfc 2881  df-ne 2935  df-ral 3058  df-rex 3059  df-rab 3062  df-v 3400  df-sbc 3681  df-csb 3791  df-dif 3846  df-un 3848  df-in 3850  df-ss 3860  df-nul 4212  df-if 4415  df-pw 4490  df-sn 4517  df-pr 4519  df-op 4523  df-uni 4797  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5429  df-po 5442  df-fr 5483  df-se 5484  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6129  df-iota 6297  df-fun 6341  df-fv 6347  df-1st 7714  df-2nd 7715
This theorem is referenced by:  on2ind  33469  no2indslem  33748
  Copyright terms: Public domain W3C validator