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

Theorem xpord3pred 8084
Description: Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 31-Jan-2025.)
Hypothesis
Ref Expression
xpord3.1 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))}
Assertion
Ref Expression
xpord3pred ((𝑋𝐴𝑌𝐵𝑍𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
Distinct variable groups:   𝑥,𝐴,𝑦   𝑥,𝐵,𝑦   𝑥,𝐶,𝑦   𝑥,𝑅,𝑦   𝑥,𝑆,𝑦   𝑥,𝑇,𝑦
Allowed substitution hints:   𝑈(𝑥,𝑦)   𝑋(𝑥,𝑦)   𝑌(𝑥,𝑦)   𝑍(𝑥,𝑦)

Proof of Theorem xpord3pred
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 𝑞 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oteq1 4839 . . . 4 (𝑎 = 𝑋 → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩)
2 predeq3 6257 . . . 4 (⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
31, 2syl 17 . . 3 (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
4 predeq3 6257 . . . . . . 7 (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5 sneq 4596 . . . . . . 7 (𝑎 = 𝑋 → {𝑎} = {𝑋})
64, 5uneq12d 4124 . . . . . 6 (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
76xpeq1d 5662 . . . . 5 (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
87xpeq1d 5662 . . . 4 (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
91sneqd 4598 . . . 4 (𝑎 = 𝑋 → {⟨𝑎, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑏, 𝑐⟩})
108, 9difeq12d 4083 . . 3 (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}))
113, 10eqeq12d 2752 . 2 (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩})))
12 oteq2 4840 . . . 4 (𝑏 = 𝑌 → ⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩)
13 predeq3 6257 . . . 4 (⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
1412, 13syl 17 . . 3 (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
15 predeq3 6257 . . . . . . 7 (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
16 sneq 4596 . . . . . . 7 (𝑏 = 𝑌 → {𝑏} = {𝑌})
1715, 16uneq12d 4124 . . . . . 6 (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
1817xpeq2d 5663 . . . . 5 (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
1918xpeq1d 5662 . . . 4 (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
2012sneqd 4598 . . . 4 (𝑏 = 𝑌 → {⟨𝑋, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑐⟩})
2119, 20difeq12d 4083 . . 3 (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}))
2214, 21eqeq12d 2752 . 2 (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩})))
23 oteq3 4841 . . . 4 (𝑐 = 𝑍 → ⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩)
24 predeq3 6257 . . . 4 (⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
2523, 24syl 17 . . 3 (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
26 predeq3 6257 . . . . . 6 (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍))
27 sneq 4596 . . . . . 6 (𝑐 = 𝑍 → {𝑐} = {𝑍})
2826, 27uneq12d 4124 . . . . 5 (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))
2928xpeq2d 5663 . . . 4 (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})))
3023sneqd 4598 . . . 4 (𝑐 = 𝑍 → {⟨𝑋, 𝑌, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑍⟩})
3129, 30difeq12d 4083 . . 3 (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
3225, 31eqeq12d 2752 . 2 (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩})))
33 el2xptp 7967 . . . . . . 7 (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩)
34 df-3an 1089 . . . . . . . . . . 11 (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
35 simplrl 775 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → 𝑑𝐴)
36 simplrr 776 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → 𝑒𝐵)
37 simpr 485 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → 𝑓𝐶)
3835, 36, 373jca 1128 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑑𝐴𝑒𝐵𝑓𝐶))
39 simpll 765 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑎𝐴𝑏𝐵𝑐𝐶))
4038, 39jca 512 . . . . . . . . . . . . 13 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)))
4140biantrurd 533 . . . . . . . . . . . 12 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
4235biantrurd 533 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑑𝑅𝑎 ↔ (𝑑𝐴𝑑𝑅𝑎)))
4342orbi1d 915 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑑𝑅𝑎𝑑 = 𝑎) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)))
4436biantrurd 533 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑒𝑆𝑏 ↔ (𝑒𝐵𝑒𝑆𝑏)))
4544orbi1d 915 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑒𝑆𝑏𝑒 = 𝑏) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
4637biantrurd 533 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑓𝑇𝑐 ↔ (𝑓𝐶𝑓𝑇𝑐)))
4746orbi1d 915 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑓𝑇𝑐𝑓 = 𝑐) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
4843, 45, 473anbi123d 1436 . . . . . . . . . . . . 13 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
4948anbi1d 630 . . . . . . . . . . . 12 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
5041, 49bitr3d 280 . . . . . . . . . . 11 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
5134, 50bitrid 282 . . . . . . . . . 10 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
52 breq1 5108 . . . . . . . . . . . 12 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ ⟨𝑑, 𝑒, 𝑓𝑈𝑎, 𝑏, 𝑐⟩))
53 xpord3.1 . . . . . . . . . . . . 13 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))}
5453xpord3lem 8081 . . . . . . . . . . . 12 (⟨𝑑, 𝑒, 𝑓𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
5552, 54bitrdi 286 . . . . . . . . . . 11 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
56 eleq1 2825 . . . . . . . . . . . 12 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
57 eldifsn 4747 . . . . . . . . . . . . 13 (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩))
58 otelxp 5676 . . . . . . . . . . . . . . 15 (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
59 elun 4108 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}))
60 vex 3449 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
6160elpred 6270 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎)))
6261elv 3451 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎))
63 velsn 4602 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎)
6462, 63orbi12i 913 . . . . . . . . . . . . . . . . 17 ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
6559, 64bitri 274 . . . . . . . . . . . . . . . 16 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
66 elun 4108 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}))
67 vex 3449 . . . . . . . . . . . . . . . . . . . 20 𝑒 ∈ V
6867elpred 6270 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏)))
6968elv 3451 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏))
70 velsn 4602 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏)
7169, 70orbi12i 913 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
7266, 71bitri 274 . . . . . . . . . . . . . . . 16 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
73 elun 4108 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}))
74 vex 3449 . . . . . . . . . . . . . . . . . . . 20 𝑓 ∈ V
7574elpred 6270 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐)))
7675elv 3451 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐))
77 velsn 4602 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐)
7876, 77orbi12i 913 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
7973, 78bitri 274 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
8065, 72, 793anbi123i 1155 . . . . . . . . . . . . . . 15 ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
8158, 80bitri 274 . . . . . . . . . . . . . 14 (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
8260, 67, 74otthne 5443 . . . . . . . . . . . . . 14 (⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩ ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
8381, 82anbi12i 627 . . . . . . . . . . . . 13 ((⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
8457, 83bitri 274 . . . . . . . . . . . 12 (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
8556, 84bitrdi 286 . . . . . . . . . . 11 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
8655, 85bibi12d 345 . . . . . . . . . 10 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
8751, 86syl5ibrcom 246 . . . . . . . . 9 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
8887rexlimdva 3152 . . . . . . . 8 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) → (∃𝑓𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
8988rexlimdvva 3205 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
9033, 89biimtrid 241 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
9190pm5.32d 577 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
92 otex 5422 . . . . . 6 𝑎, 𝑏, 𝑐⟩ ∈ V
93 vex 3449 . . . . . . 7 𝑞 ∈ V
9493elpred 6270 . . . . . 6 (⟨𝑎, 𝑏, 𝑐⟩ ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈𝑎, 𝑏, 𝑐⟩)))
9592, 94ax-mp 5 . . . . 5 (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
96 elin 3926 . . . . 5 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
9791, 95, 963bitr4g 313 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
9897eqrdv 2734 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
99 predss 6261 . . . . . . . . . 10 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
10099a1i 11 . . . . . . . . 9 (𝑎𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
101 snssi 4768 . . . . . . . . 9 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
102100, 101unssd 4146 . . . . . . . 8 (𝑎𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
1031023ad2ant1 1133 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
104 predss 6261 . . . . . . . . . 10 Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
105104a1i 11 . . . . . . . . 9 (𝑏𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
106 snssi 4768 . . . . . . . . 9 (𝑏𝐵 → {𝑏} ⊆ 𝐵)
107105, 106unssd 4146 . . . . . . . 8 (𝑏𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
1081073ad2ant2 1134 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
109 xpss12 5648 . . . . . . 7 (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
110103, 108, 109syl2anc 584 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
111 predss 6261 . . . . . . . . 9 Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶
112111a1i 11 . . . . . . . 8 (𝑐𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶)
113 snssi 4768 . . . . . . . 8 (𝑐𝐶 → {𝑐} ⊆ 𝐶)
114112, 113unssd 4146 . . . . . . 7 (𝑐𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
1151143ad2ant3 1135 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
116 xpss12 5648 . . . . . 6 ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
117110, 115, 116syl2anc 584 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
118117ssdifssd 4102 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶))
119 sseqin2 4175 . . . 4 (((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
120118, 119sylib 217 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
12198, 120eqtrd 2776 . 2 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
12211, 22, 32, 121vtocl3ga 3538 1 ((𝑋𝐴𝑌𝐵𝑍𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  wo 845  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  wne 2943  wrex 3073  Vcvv 3445  cdif 3907  cun 3908  cin 3909  wss 3910  {csn 4586  cotp 4594   class class class wbr 5105  {copab 5167   × cxp 5631  Predcpred 6252  cfv 6496  1st c1st 7919  2nd c2nd 7920
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-ot 4595  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-iota 6448  df-fun 6498  df-fv 6504  df-1st 7921  df-2nd 7922
This theorem is referenced by:  sexp3  8085  xpord3inddlem  8086
  Copyright terms: Public domain W3C validator