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

Theorem xpord3pred 8176
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 4887 . . . 4 (𝑎 = 𝑋 → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩)
2 predeq3 6327 . . . 4 (⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
31, 2syl 17 . . 3 (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
4 predeq3 6327 . . . . . . 7 (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5 sneq 4641 . . . . . . 7 (𝑎 = 𝑋 → {𝑎} = {𝑋})
64, 5uneq12d 4179 . . . . . 6 (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
76xpeq1d 5718 . . . . 5 (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
87xpeq1d 5718 . . . 4 (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
91sneqd 4643 . . . 4 (𝑎 = 𝑋 → {⟨𝑎, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑏, 𝑐⟩})
108, 9difeq12d 4137 . . 3 (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}))
113, 10eqeq12d 2751 . 2 (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩})))
12 oteq2 4888 . . . 4 (𝑏 = 𝑌 → ⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩)
13 predeq3 6327 . . . 4 (⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
1412, 13syl 17 . . 3 (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
15 predeq3 6327 . . . . . . 7 (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
16 sneq 4641 . . . . . . 7 (𝑏 = 𝑌 → {𝑏} = {𝑌})
1715, 16uneq12d 4179 . . . . . 6 (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
1817xpeq2d 5719 . . . . 5 (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
1918xpeq1d 5718 . . . 4 (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
2012sneqd 4643 . . . 4 (𝑏 = 𝑌 → {⟨𝑋, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑐⟩})
2119, 20difeq12d 4137 . . 3 (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}))
2214, 21eqeq12d 2751 . 2 (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩})))
23 oteq3 4889 . . . 4 (𝑐 = 𝑍 → ⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩)
24 predeq3 6327 . . . 4 (⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
2523, 24syl 17 . . 3 (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
26 predeq3 6327 . . . . . 6 (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍))
27 sneq 4641 . . . . . 6 (𝑐 = 𝑍 → {𝑐} = {𝑍})
2826, 27uneq12d 4179 . . . . 5 (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))
2928xpeq2d 5719 . . . 4 (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})))
3023sneqd 4643 . . . 4 (𝑐 = 𝑍 → {⟨𝑋, 𝑌, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑍⟩})
3129, 30difeq12d 4137 . . 3 (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
3225, 31eqeq12d 2751 . 2 (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩})))
33 el2xptp 8059 . . . . . . 7 (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩)
34 df-3an 1088 . . . . . . . . . . 11 (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
35 simplrl 777 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → 𝑑𝐴)
36 simplrr 778 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → 𝑒𝐵)
37 simpr 484 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → 𝑓𝐶)
3835, 36, 373jca 1127 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑑𝐴𝑒𝐵𝑓𝐶))
39 simpll 767 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑎𝐴𝑏𝐵𝑐𝐶))
4038, 39jca 511 . . . . . . . . . . . . 13 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)))
4140biantrurd 532 . . . . . . . . . . . 12 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
4235biantrurd 532 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑑𝑅𝑎 ↔ (𝑑𝐴𝑑𝑅𝑎)))
4342orbi1d 916 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑑𝑅𝑎𝑑 = 𝑎) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)))
4436biantrurd 532 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑒𝑆𝑏 ↔ (𝑒𝐵𝑒𝑆𝑏)))
4544orbi1d 916 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑒𝑆𝑏𝑒 = 𝑏) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
4637biantrurd 532 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑓𝑇𝑐 ↔ (𝑓𝐶𝑓𝑇𝑐)))
4746orbi1d 916 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑓𝑇𝑐𝑓 = 𝑐) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
4843, 45, 473anbi123d 1435 . . . . . . . . . . . . 13 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
4948anbi1d 631 . . . . . . . . . . . 12 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
5041, 49bitr3d 281 . . . . . . . . . . 11 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
5134, 50bitrid 283 . . . . . . . . . 10 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
52 breq1 5151 . . . . . . . . . . . 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 8173 . . . . . . . . . . . 12 (⟨𝑑, 𝑒, 𝑓𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
5552, 54bitrdi 287 . . . . . . . . . . 11 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
56 eleq1 2827 . . . . . . . . . . . 12 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
57 eldifsn 4791 . . . . . . . . . . . . 13 (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩))
58 otelxp 5733 . . . . . . . . . . . . . . 15 (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
59 elun 4163 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}))
60 vex 3482 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
6160elpred 6340 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎)))
6261elv 3483 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎))
63 velsn 4647 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎)
6462, 63orbi12i 914 . . . . . . . . . . . . . . . . 17 ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
6559, 64bitri 275 . . . . . . . . . . . . . . . 16 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
66 elun 4163 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}))
67 vex 3482 . . . . . . . . . . . . . . . . . . . 20 𝑒 ∈ V
6867elpred 6340 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏)))
6968elv 3483 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏))
70 velsn 4647 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏)
7169, 70orbi12i 914 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
7266, 71bitri 275 . . . . . . . . . . . . . . . 16 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
73 elun 4163 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}))
74 vex 3482 . . . . . . . . . . . . . . . . . . . 20 𝑓 ∈ V
7574elpred 6340 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐)))
7675elv 3483 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐))
77 velsn 4647 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐)
7876, 77orbi12i 914 . . . . . . . . . . . . . . . . 17 ((𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
7973, 78bitri 275 . . . . . . . . . . . . . . . 16 (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
8065, 72, 793anbi123i 1154 . . . . . . . . . . . . . . 15 ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
8158, 80bitri 275 . . . . . . . . . . . . . 14 (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
8260, 67, 74otthne 5497 . . . . . . . . . . . . . 14 (⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩ ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
8381, 82anbi12i 628 . . . . . . . . . . . . 13 ((⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
8457, 83bitri 275 . . . . . . . . . . . 12 (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
8556, 84bitrdi 287 . . . . . . . . . . 11 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
8655, 85bibi12d 345 . . . . . . . . . 10 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → ((𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
8751, 86syl5ibrcom 247 . . . . . . . . 9 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
8887rexlimdva 3153 . . . . . . . 8 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) → (∃𝑓𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
8988rexlimdvva 3211 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
9033, 89biimtrid 242 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
9190pm5.32d 577 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
92 otex 5476 . . . . . 6 𝑎, 𝑏, 𝑐⟩ ∈ V
93 vex 3482 . . . . . . 7 𝑞 ∈ V
9493elpred 6340 . . . . . 6 (⟨𝑎, 𝑏, 𝑐⟩ ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈𝑎, 𝑏, 𝑐⟩)))
9592, 94ax-mp 5 . . . . 5 (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
96 elin 3979 . . . . 5 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
9791, 95, 963bitr4g 314 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
9897eqrdv 2733 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
99 predss 6331 . . . . . . . . . 10 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
10099a1i 11 . . . . . . . . 9 (𝑎𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
101 snssi 4813 . . . . . . . . 9 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
102100, 101unssd 4202 . . . . . . . 8 (𝑎𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
1031023ad2ant1 1132 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
104 predss 6331 . . . . . . . . . 10 Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
105104a1i 11 . . . . . . . . 9 (𝑏𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
106 snssi 4813 . . . . . . . . 9 (𝑏𝐵 → {𝑏} ⊆ 𝐵)
107105, 106unssd 4202 . . . . . . . 8 (𝑏𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
1081073ad2ant2 1133 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
109 xpss12 5704 . . . . . . 7 (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
110103, 108, 109syl2anc 584 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
111 predss 6331 . . . . . . . . 9 Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶
112111a1i 11 . . . . . . . 8 (𝑐𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶)
113 snssi 4813 . . . . . . . 8 (𝑐𝐶 → {𝑐} ⊆ 𝐶)
114112, 113unssd 4202 . . . . . . 7 (𝑐𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
1151143ad2ant3 1134 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
116 xpss12 5704 . . . . . 6 ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
117110, 115, 116syl2anc 584 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
118117ssdifssd 4157 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶))
119 sseqin2 4231 . . . 4 (((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
120118, 119sylib 218 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
12198, 120eqtrd 2775 . 2 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
12211, 22, 32, 121vtocl3ga 3583 1 ((𝑋𝐴𝑌𝐵𝑍𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  wo 847  w3o 1085  w3a 1086   = wceq 1537  wcel 2106  wne 2938  wrex 3068  Vcvv 3478  cdif 3960  cun 3961  cin 3962  wss 3963  {csn 4631  cotp 4639   class class class wbr 5148  {copab 5210   × cxp 5687  Predcpred 6322  cfv 6563  1st c1st 8011  2nd c2nd 8012
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438  ax-un 7754
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-ot 4640  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-iota 6516  df-fun 6565  df-fv 6571  df-1st 8013  df-2nd 8014
This theorem is referenced by:  sexp3  8177  xpord3inddlem  8178
  Copyright terms: Public domain W3C validator