MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  xpord2pred Structured version   Visualization version   GIF version

Theorem xpord2pred 8170
Description: Calculate the predecessor class in frxp2 8169. (Contributed by Scott Fenton, 22-Aug-2024.)
Hypothesis
Ref Expression
xpord2.1 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st𝑥)𝑅(1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥)𝑆(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}
Assertion
Ref Expression
xpord2pred ((𝑋𝐴𝑌𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦
Allowed substitution hints:   𝑇(𝑥,𝑦)   𝑋(𝑥,𝑦)   𝑌(𝑥,𝑦)

Proof of Theorem xpord2pred
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opeq1 4873 . . . 4 (𝑎 = 𝑋 → ⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩)
2 predeq3 6325 . . . 4 (⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
31, 2syl 17 . . 3 (𝑎 = 𝑋 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
4 predeq3 6325 . . . . . 6 (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5 sneq 4636 . . . . . 6 (𝑎 = 𝑋 → {𝑎} = {𝑋})
64, 5uneq12d 4169 . . . . 5 (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
76xpeq1d 5714 . . . 4 (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
81sneqd 4638 . . . 4 (𝑎 = 𝑋 → {⟨𝑎, 𝑏⟩} = {⟨𝑋, 𝑏⟩})
97, 8difeq12d 4127 . . 3 (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}))
103, 9eqeq12d 2753 . 2 (𝑎 = 𝑋 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩})))
11 opeq2 4874 . . . 4 (𝑏 = 𝑌 → ⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩)
12 predeq3 6325 . . . 4 (⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
1311, 12syl 17 . . 3 (𝑏 = 𝑌 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
14 predeq3 6325 . . . . . 6 (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
15 sneq 4636 . . . . . 6 (𝑏 = 𝑌 → {𝑏} = {𝑌})
1614, 15uneq12d 4169 . . . . 5 (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
1716xpeq2d 5715 . . . 4 (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
1811sneqd 4638 . . . 4 (𝑏 = 𝑌 → {⟨𝑋, 𝑏⟩} = {⟨𝑋, 𝑌⟩})
1917, 18difeq12d 4127 . . 3 (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
2013, 19eqeq12d 2753 . 2 (𝑏 = 𝑌 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩})))
21 predel 6342 . . . . 5 (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵))
2221a1i 11 . . . 4 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵)))
23 eldifi 4131 . . . . 5 (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
24 predss 6329 . . . . . . . . 9 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
2524a1i 11 . . . . . . . 8 (𝑎𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
26 snssi 4808 . . . . . . . 8 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
2725, 26unssd 4192 . . . . . . 7 (𝑎𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
28 predss 6329 . . . . . . . . 9 Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
2928a1i 11 . . . . . . . 8 (𝑏𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
30 snssi 4808 . . . . . . . 8 (𝑏𝐵 → {𝑏} ⊆ 𝐵)
3129, 30unssd 4192 . . . . . . 7 (𝑏𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
32 xpss12 5700 . . . . . . 7 (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
3327, 31, 32syl2an 596 . . . . . 6 ((𝑎𝐴𝑏𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
3433sseld 3982 . . . . 5 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → 𝑒 ∈ (𝐴 × 𝐵)))
3523, 34syl5 34 . . . 4 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ (𝐴 × 𝐵)))
36 elxp2 5709 . . . . 5 (𝑒 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝐴𝑑𝐵 𝑒 = ⟨𝑐, 𝑑⟩)
37 opex 5469 . . . . . . . . 9 𝑎, 𝑏⟩ ∈ V
38 opex 5469 . . . . . . . . . 10 𝑐, 𝑑⟩ ∈ V
3938elpred 6338 . . . . . . . . 9 (⟨𝑎, 𝑏⟩ ∈ V → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩)))
4037, 39ax-mp 5 . . . . . . . 8 (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
41 opelxpi 5722 . . . . . . . . . . 11 ((𝑐𝐴𝑑𝐵) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
4241adantl 481 . . . . . . . . . 10 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
4342biantrurd 532 . . . . . . . . 9 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩ ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩)))
44 xpord2.1 . . . . . . . . . . 11 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st𝑥)𝑅(1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥)𝑆(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}
4544xpord2lem 8167 . . . . . . . . . 10 (⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩ ↔ ((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵) ∧ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))))
46 eldif 3961 . . . . . . . . . . . . 13 (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}))
47 opelxp 5721 . . . . . . . . . . . . . . 15 (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
48 elun 4153 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}))
49 vex 3484 . . . . . . . . . . . . . . . . . . . 20 𝑐 ∈ V
5049elpred 6338 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ V → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐𝐴𝑐𝑅𝑎)))
5150elv 3485 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐𝐴𝑐𝑅𝑎))
52 velsn 4642 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ {𝑎} ↔ 𝑐 = 𝑎)
5351, 52orbi12i 915 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}) ↔ ((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
5448, 53bitri 275 . . . . . . . . . . . . . . . 16 (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
55 elun 4153 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}))
56 vex 3484 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
5756elpred 6338 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ V → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑𝐵𝑑𝑆𝑏)))
5857elv 3485 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑𝐵𝑑𝑆𝑏))
59 velsn 4642 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ {𝑏} ↔ 𝑑 = 𝑏)
6058, 59orbi12i 915 . . . . . . . . . . . . . . . . 17 ((𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}) ↔ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
6155, 60bitri 275 . . . . . . . . . . . . . . . 16 (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
6254, 61anbi12i 628 . . . . . . . . . . . . . . 15 ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
6347, 62bitri 275 . . . . . . . . . . . . . 14 (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
6438elsn 4641 . . . . . . . . . . . . . . . 16 (⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
6564notbii 320 . . . . . . . . . . . . . . 15 (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66 df-ne 2941 . . . . . . . . . . . . . . 15 (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
6749, 56opthne 5487 . . . . . . . . . . . . . . 15 (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ (𝑐𝑎𝑑𝑏))
6865, 66, 673bitr2i 299 . . . . . . . . . . . . . 14 (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ (𝑐𝑎𝑑𝑏))
6963, 68anbi12i 628 . . . . . . . . . . . . 13 ((⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐𝑎𝑑𝑏)))
7046, 69bitri 275 . . . . . . . . . . . 12 (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐𝑎𝑑𝑏)))
71 simprl 771 . . . . . . . . . . . . . . . 16 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → 𝑐𝐴)
7271biantrurd 532 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (𝑐𝑅𝑎 ↔ (𝑐𝐴𝑐𝑅𝑎)))
7372orbi1d 917 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑐𝑅𝑎𝑐 = 𝑎) ↔ ((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎)))
74 simprr 773 . . . . . . . . . . . . . . . 16 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → 𝑑𝐵)
7574biantrurd 532 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (𝑑𝑆𝑏 ↔ (𝑑𝐵𝑑𝑆𝑏)))
7675orbi1d 917 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑑𝑆𝑏𝑑 = 𝑏) ↔ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
7773, 763anbi12d 1439 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)) ↔ (((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))))
78 df-3an 1089 . . . . . . . . . . . . 13 ((((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)) ↔ ((((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐𝑎𝑑𝑏)))
7977, 78bitr2di 288 . . . . . . . . . . . 12 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (((((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐𝑎𝑑𝑏)) ↔ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))))
8070, 79bitrid 283 . . . . . . . . . . 11 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))))
81 pm3.22 459 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵)))
8281biantrurd 532 . . . . . . . . . . . 12 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)) ↔ (((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵)) ∧ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)))))
83 df-3an 1089 . . . . . . . . . . . 12 (((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵) ∧ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))) ↔ (((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵)) ∧ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))))
8482, 83bitr4di 289 . . . . . . . . . . 11 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)) ↔ ((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵) ∧ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)))))
8580, 84bitr2d 280 . . . . . . . . . 10 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵) ∧ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
8645, 85bitrid 283 . . . . . . . . 9 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩ ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
8743, 86bitr3d 281 . . . . . . . 8 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
8840, 87bitrid 283 . . . . . . 7 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
89 eleq1 2829 . . . . . . . 8 (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩)))
90 eleq1 2829 . . . . . . . 8 (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
9189, 90bibi12d 345 . . . . . . 7 (𝑒 = ⟨𝑐, 𝑑⟩ → ((𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})) ↔ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
9288, 91syl5ibrcom 247 . . . . . 6 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
9392rexlimdvva 3213 . . . . 5 ((𝑎𝐴𝑏𝐵) → (∃𝑐𝐴𝑑𝐵 𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
9436, 93biimtrid 242 . . . 4 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ (𝐴 × 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
9522, 35, 94pm5.21ndd 379 . . 3 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
9695eqrdv 2735 . 2 ((𝑎𝐴𝑏𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))
9710, 20, 96vtocl2ga 3578 1 ((𝑋𝐴𝑌𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wrex 3070  Vcvv 3480  cdif 3948  cun 3949  wss 3951  {csn 4626  cop 4632   class class class wbr 5143  {copab 5205   × cxp 5683  Predcpred 6320  cfv 6561  1st c1st 8012  2nd c2nd 8013
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-iota 6514  df-fun 6563  df-fv 6569  df-1st 8014  df-2nd 8015
This theorem is referenced by:  sexp2  8171  xpord2indlem  8172  on2recsov  8706  noxpordpred  27986
  Copyright terms: Public domain W3C validator