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

Theorem xpord2pred 8168
Description: Calculate the predecessor class in frxp2 8167. (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 4877 . . . 4 (𝑎 = 𝑋 → ⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩)
2 predeq3 6326 . . . 4 (⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
31, 2syl 17 . . 3 (𝑎 = 𝑋 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩))
4 predeq3 6326 . . . . . 6 (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5 sneq 4640 . . . . . 6 (𝑎 = 𝑋 → {𝑎} = {𝑋})
64, 5uneq12d 4178 . . . . 5 (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
76xpeq1d 5717 . . . 4 (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
81sneqd 4642 . . . 4 (𝑎 = 𝑋 → {⟨𝑎, 𝑏⟩} = {⟨𝑋, 𝑏⟩})
97, 8difeq12d 4136 . . 3 (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}))
103, 9eqeq12d 2750 . 2 (𝑎 = 𝑋 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩})))
11 opeq2 4878 . . . 4 (𝑏 = 𝑌 → ⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩)
12 predeq3 6326 . . . 4 (⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩ → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
1311, 12syl 17 . . 3 (𝑏 = 𝑌 → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩))
14 predeq3 6326 . . . . . 6 (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
15 sneq 4640 . . . . . 6 (𝑏 = 𝑌 → {𝑏} = {𝑌})
1614, 15uneq12d 4178 . . . . 5 (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
1716xpeq2d 5718 . . . 4 (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
1811sneqd 4642 . . . 4 (𝑏 = 𝑌 → {⟨𝑋, 𝑏⟩} = {⟨𝑋, 𝑌⟩})
1917, 18difeq12d 4136 . . 3 (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
2013, 19eqeq12d 2750 . 2 (𝑏 = 𝑌 → (Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑋, 𝑏⟩}) ↔ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩})))
21 predel 6343 . . . . 5 (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵))
2221a1i 11 . . . 4 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) → 𝑒 ∈ (𝐴 × 𝐵)))
23 eldifi 4140 . . . . 5 (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
24 predss 6330 . . . . . . . . 9 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
2524a1i 11 . . . . . . . 8 (𝑎𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
26 snssi 4812 . . . . . . . 8 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
2725, 26unssd 4201 . . . . . . 7 (𝑎𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
28 predss 6330 . . . . . . . . 9 Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
2928a1i 11 . . . . . . . 8 (𝑏𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
30 snssi 4812 . . . . . . . 8 (𝑏𝐵 → {𝑏} ⊆ 𝐵)
3129, 30unssd 4201 . . . . . . 7 (𝑏𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
32 xpss12 5703 . . . . . . 7 (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
3327, 31, 32syl2an 596 . . . . . 6 ((𝑎𝐴𝑏𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
3433sseld 3993 . . . . 5 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) → 𝑒 ∈ (𝐴 × 𝐵)))
3523, 34syl5 34 . . . 4 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) → 𝑒 ∈ (𝐴 × 𝐵)))
36 elxp2 5712 . . . . 5 (𝑒 ∈ (𝐴 × 𝐵) ↔ ∃𝑐𝐴𝑑𝐵 𝑒 = ⟨𝑐, 𝑑⟩)
37 opex 5474 . . . . . . . . 9 𝑎, 𝑏⟩ ∈ V
38 opex 5474 . . . . . . . . . 10 𝑐, 𝑑⟩ ∈ V
3938elpred 6339 . . . . . . . . 9 (⟨𝑎, 𝑏⟩ ∈ V → (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩)))
4037, 39ax-mp 5 . . . . . . . 8 (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩))
41 opelxpi 5725 . . . . . . . . . . 11 ((𝑐𝐴𝑑𝐵) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
4241adantl 481 . . . . . . . . . 10 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵))
4342biantrurd 532 . . . . . . . . 9 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩ ↔ (⟨𝑐, 𝑑⟩ ∈ (𝐴 × 𝐵) ∧ ⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩)))
44 xpord2.1 . . . . . . . . . . 11 𝑇 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ (𝐴 × 𝐵) ∧ 𝑦 ∈ (𝐴 × 𝐵) ∧ (((1st𝑥)𝑅(1st𝑦) ∨ (1st𝑥) = (1st𝑦)) ∧ ((2nd𝑥)𝑆(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦)) ∧ 𝑥𝑦))}
4544xpord2lem 8165 . . . . . . . . . 10 (⟨𝑐, 𝑑𝑇𝑎, 𝑏⟩ ↔ ((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵) ∧ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))))
46 eldif 3972 . . . . . . . . . . . . 13 (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ ¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩}))
47 opelxp 5724 . . . . . . . . . . . . . . 15 (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
48 elun 4162 . . . . . . . . . . . . . . . . 17 (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}))
49 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑐 ∈ V
5049elpred 6339 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ V → (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐𝐴𝑐𝑅𝑎)))
5150elv 3482 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑐𝐴𝑐𝑅𝑎))
52 velsn 4646 . . . . . . . . . . . . . . . . . 18 (𝑐 ∈ {𝑎} ↔ 𝑐 = 𝑎)
5351, 52orbi12i 914 . . . . . . . . . . . . . . . . 17 ((𝑐 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑐 ∈ {𝑎}) ↔ ((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
5448, 53bitri 275 . . . . . . . . . . . . . . . 16 (𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎))
55 elun 4162 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}))
56 vex 3481 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
5756elpred 6339 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ V → (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑𝐵𝑑𝑆𝑏)))
5857elv 3482 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑑𝐵𝑑𝑆𝑏))
59 velsn 4646 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ {𝑏} ↔ 𝑑 = 𝑏)
6058, 59orbi12i 914 . . . . . . . . . . . . . . . . 17 ((𝑑 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑑 ∈ {𝑏}) ↔ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
6155, 60bitri 275 . . . . . . . . . . . . . . . 16 (𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏))
6254, 61anbi12i 628 . . . . . . . . . . . . . . 15 ((𝑐 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑑 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
6347, 62bitri 275 . . . . . . . . . . . . . 14 (⟨𝑐, 𝑑⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
6438elsn 4645 . . . . . . . . . . . . . . . 16 (⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
6564notbii 320 . . . . . . . . . . . . . . 15 (¬ ⟨𝑐, 𝑑⟩ ∈ {⟨𝑎, 𝑏⟩} ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
66 df-ne 2938 . . . . . . . . . . . . . . 15 (⟨𝑐, 𝑑⟩ ≠ ⟨𝑎, 𝑏⟩ ↔ ¬ ⟨𝑐, 𝑑⟩ = ⟨𝑎, 𝑏⟩)
6749, 56opthne 5492 . . . . . . . . . . . . . . 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 916 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑐𝑅𝑎𝑐 = 𝑎) ↔ ((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎)))
74 simprr 773 . . . . . . . . . . . . . . . 16 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → 𝑑𝐵)
7574biantrurd 532 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (𝑑𝑆𝑏 ↔ (𝑑𝐵𝑑𝑆𝑏)))
7675orbi1d 916 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑑𝑆𝑏𝑑 = 𝑏) ↔ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)))
7773, 763anbi12d 1436 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)) ↔ (((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))))
78 df-3an 1088 . . . . . . . . . . . . 13 ((((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)) ↔ ((((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐𝑎𝑑𝑏)))
7977, 78bitr2di 288 . . . . . . . . . . . 12 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (((((𝑐𝐴𝑐𝑅𝑎) ∨ 𝑐 = 𝑎) ∧ ((𝑑𝐵𝑑𝑆𝑏) ∨ 𝑑 = 𝑏)) ∧ (𝑐𝑎𝑑𝑏)) ↔ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))))
8070, 79bitrid 283 . . . . . . . . . . 11 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏))))
81 pm3.22 459 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → ((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵)))
8281biantrurd 532 . . . . . . . . . . . 12 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)) ↔ (((𝑐𝐴𝑑𝐵) ∧ (𝑎𝐴𝑏𝐵)) ∧ ((𝑐𝑅𝑎𝑐 = 𝑎) ∧ (𝑑𝑆𝑏𝑑 = 𝑏) ∧ (𝑐𝑎𝑑𝑏)))))
83 df-3an 1088 . . . . . . . . . . . 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 2826 . . . . . . . 8 (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩)))
90 eleq1 2826 . . . . . . . 8 (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
9189, 90bibi12d 345 . . . . . . 7 (𝑒 = ⟨𝑐, 𝑑⟩ → ((𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})) ↔ (⟨𝑐, 𝑑⟩ ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ ⟨𝑐, 𝑑⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
9288, 91syl5ibrcom 247 . . . . . 6 (((𝑎𝐴𝑏𝐵) ∧ (𝑐𝐴𝑑𝐵)) → (𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
9392rexlimdvva 3210 . . . . 5 ((𝑎𝐴𝑏𝐵) → (∃𝑐𝐴𝑑𝐵 𝑒 = ⟨𝑐, 𝑑⟩ → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
9436, 93biimtrid 242 . . . 4 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ (𝐴 × 𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))))
9522, 35, 94pm5.21ndd 379 . . 3 ((𝑎𝐴𝑏𝐵) → (𝑒 ∈ Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) ↔ 𝑒 ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩})))
9695eqrdv 2732 . 2 ((𝑎𝐴𝑏𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑎, 𝑏⟩) = (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∖ {⟨𝑎, 𝑏⟩}))
9710, 20, 96vtocl2ga 3577 1 ((𝑋𝐴𝑌𝐵) → Pred(𝑇, (𝐴 × 𝐵), ⟨𝑋, 𝑌⟩) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) ∖ {⟨𝑋, 𝑌⟩}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 847  w3a 1086   = wceq 1536  wcel 2105  wne 2937  wrex 3067  Vcvv 3477  cdif 3959  cun 3960  wss 3962  {csn 4630  cop 4636   class class class wbr 5147  {copab 5209   × cxp 5686  Predcpred 6321  cfv 6562  1st c1st 8010  2nd c2nd 8011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-iota 6515  df-fun 6564  df-fv 6570  df-1st 8012  df-2nd 8013
This theorem is referenced by:  sexp2  8169  xpord2indlem  8170  on2recsov  8704  noxpordpred  28000
  Copyright terms: Public domain W3C validator