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

Theorem xpord3pred 8143
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 4882 . . . 4 (𝑎 = 𝑋 → ⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩)
2 predeq3 6304 . . . 4 (⟨𝑎, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑏, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
31, 2syl 17 . . 3 (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩))
4 predeq3 6304 . . . . . . 7 (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
5 sneq 4638 . . . . . . 7 (𝑎 = 𝑋 → {𝑎} = {𝑋})
64, 5uneq12d 4164 . . . . . 6 (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
76xpeq1d 5705 . . . . 5 (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
87xpeq1d 5705 . . . 4 (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
91sneqd 4640 . . . 4 (𝑎 = 𝑋 → {⟨𝑎, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑏, 𝑐⟩})
108, 9difeq12d 4123 . . 3 (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}))
113, 10eqeq12d 2747 . 2 (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩})))
12 oteq2 4883 . . . 4 (𝑏 = 𝑌 → ⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩)
13 predeq3 6304 . . . 4 (⟨𝑋, 𝑏, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
1412, 13syl 17 . . 3 (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩))
15 predeq3 6304 . . . . . . 7 (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
16 sneq 4638 . . . . . . 7 (𝑏 = 𝑌 → {𝑏} = {𝑌})
1715, 16uneq12d 4164 . . . . . 6 (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
1817xpeq2d 5706 . . . . 5 (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
1918xpeq1d 5705 . . . 4 (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
2012sneqd 4640 . . . 4 (𝑏 = 𝑌 → {⟨𝑋, 𝑏, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑐⟩})
2119, 20difeq12d 4123 . . 3 (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}))
2214, 21eqeq12d 2747 . 2 (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑏, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩})))
23 oteq3 4884 . . . 4 (𝑐 = 𝑍 → ⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩)
24 predeq3 6304 . . . 4 (⟨𝑋, 𝑌, 𝑐⟩ = ⟨𝑋, 𝑌, 𝑍⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
2523, 24syl 17 . . 3 (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩))
26 predeq3 6304 . . . . . 6 (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍))
27 sneq 4638 . . . . . 6 (𝑐 = 𝑍 → {𝑐} = {𝑍})
2826, 27uneq12d 4164 . . . . 5 (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))
2928xpeq2d 5706 . . . 4 (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})))
3023sneqd 4640 . . . 4 (𝑐 = 𝑍 → {⟨𝑋, 𝑌, 𝑐⟩} = {⟨𝑋, 𝑌, 𝑍⟩})
3129, 30difeq12d 4123 . . 3 (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
3225, 31eqeq12d 2747 . 2 (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑋, 𝑌, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩})))
33 el2xptp 8025 . . . . . . 7 (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩)
34 df-3an 1088 . . . . . . . . . . 11 (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
35 simplrl 774 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → 𝑑𝐴)
36 simplrr 775 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → 𝑒𝐵)
37 simpr 484 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → 𝑓𝐶)
3835, 36, 373jca 1127 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑑𝐴𝑒𝐵𝑓𝐶))
39 simpll 764 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑎𝐴𝑏𝐵𝑐𝐶))
4038, 39jca 511 . . . . . . . . . . . . 13 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)))
4140biantrurd 532 . . . . . . . . . . . 12 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
4235biantrurd 532 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑑𝑅𝑎 ↔ (𝑑𝐴𝑑𝑅𝑎)))
4342orbi1d 914 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑑𝑅𝑎𝑑 = 𝑎) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)))
4436biantrurd 532 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑒𝑆𝑏 ↔ (𝑒𝐵𝑒𝑆𝑏)))
4544orbi1d 914 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑒𝑆𝑏𝑒 = 𝑏) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
4637biantrurd 532 . . . . . . . . . . . . . . 15 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑓𝑇𝑐 ↔ (𝑓𝐶𝑓𝑇𝑐)))
4746orbi1d 914 . . . . . . . . . . . . . 14 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → ((𝑓𝑇𝑐𝑓 = 𝑐) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
4843, 45, 473anbi123d 1435 . . . . . . . . . . . . 13 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
4948anbi1d 629 . . . . . . . . . . . 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 8140 . . . . . . . . . . . 12 (⟨𝑑, 𝑒, 𝑓𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
5552, 54bitrdi 287 . . . . . . . . . . 11 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
56 eleq1 2820 . . . . . . . . . . . 12 (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ ⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
57 eldifsn 4790 . . . . . . . . . . . . 13 (⟨𝑑, 𝑒, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ↔ (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩))
58 otelxp 5720 . . . . . . . . . . . . . . 15 (⟨𝑑, 𝑒, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
59 elun 4148 . . . . . . . . . . . . . . . . 17 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}))
60 vex 3477 . . . . . . . . . . . . . . . . . . . 20 𝑑 ∈ V
6160elpred 6317 . . . . . . . . . . . . . . . . . . 19 (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎)))
6261elv 3479 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎))
63 velsn 4644 . . . . . . . . . . . . . . . . . 18 (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎)
6462, 63orbi12i 912 . . . . . . . . . . . . . . . . 17 ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
6559, 64bitri 275 . . . . . . . . . . . . . . . 16 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
66 elun 4148 . . . . . . . . . . . . . . . . 17 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}))
67 vex 3477 . . . . . . . . . . . . . . . . . . . 20 𝑒 ∈ V
6867elpred 6317 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏)))
6968elv 3479 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏))
70 velsn 4644 . . . . . . . . . . . . . . . . . 18 (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏)
7169, 70orbi12i 912 . . . . . . . . . . . . . . . . 17 ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
7266, 71bitri 275 . . . . . . . . . . . . . . . 16 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
73 elun 4148 . . . . . . . . . . . . . . . . 17 (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}))
74 vex 3477 . . . . . . . . . . . . . . . . . . . 20 𝑓 ∈ V
7574elpred 6317 . . . . . . . . . . . . . . . . . . 19 (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐)))
7675elv 3479 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐))
77 velsn 4644 . . . . . . . . . . . . . . . . . 18 (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐)
7876, 77orbi12i 912 . . . . . . . . . . . . . . . . 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 5486 . . . . . . . . . . . . . 14 (⟨𝑑, 𝑒, 𝑓⟩ ≠ ⟨𝑎, 𝑏, 𝑐⟩ ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
8381, 82anbi12i 626 . . . . . . . . . . . . 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 246 . . . . . . . . 9 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
8887rexlimdva 3154 . . . . . . . 8 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) → (∃𝑓𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
8988rexlimdvva 3210 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨𝑑, 𝑒, 𝑓⟩ → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
9033, 89biimtrid 241 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈𝑎, 𝑏, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
9190pm5.32d 576 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
92 otex 5465 . . . . . 6 𝑎, 𝑏, 𝑐⟩ ∈ V
93 vex 3477 . . . . . . 7 𝑞 ∈ V
9493elpred 6317 . . . . . 6 (⟨𝑎, 𝑏, 𝑐⟩ ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈𝑎, 𝑏, 𝑐⟩)))
9592, 94ax-mp 5 . . . . 5 (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈𝑎, 𝑏, 𝑐⟩))
96 elin 3964 . . . . 5 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
9791, 95, 963bitr4g 314 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))))
9897eqrdv 2729 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})))
99 predss 6308 . . . . . . . . . 10 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
10099a1i 11 . . . . . . . . 9 (𝑎𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
101 snssi 4811 . . . . . . . . 9 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
102100, 101unssd 4186 . . . . . . . 8 (𝑎𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
1031023ad2ant1 1132 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
104 predss 6308 . . . . . . . . . 10 Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
105104a1i 11 . . . . . . . . 9 (𝑏𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
106 snssi 4811 . . . . . . . . 9 (𝑏𝐵 → {𝑏} ⊆ 𝐵)
107105, 106unssd 4186 . . . . . . . 8 (𝑏𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
1081073ad2ant2 1133 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
109 xpss12 5691 . . . . . . 7 (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
110103, 108, 109syl2anc 583 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
111 predss 6308 . . . . . . . . 9 Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶
112111a1i 11 . . . . . . . 8 (𝑐𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶)
113 snssi 4811 . . . . . . . 8 (𝑐𝐶 → {𝑐} ⊆ 𝐶)
114112, 113unssd 4186 . . . . . . 7 (𝑐𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
1151143ad2ant3 1134 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
116 xpss12 5691 . . . . . 6 ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
117110, 115, 116syl2anc 583 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
118117ssdifssd 4142 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶))
119 sseqin2 4215 . . . 4 (((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
120118, 119sylib 217 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
12198, 120eqtrd 2771 . 2 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑎, 𝑏, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨𝑎, 𝑏, 𝑐⟩}))
12211, 22, 32, 121vtocl3ga 3570 1 ((𝑋𝐴𝑌𝐵𝑍𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨𝑋, 𝑌, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨𝑋, 𝑌, 𝑍⟩}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  wo 844  w3o 1085  w3a 1086   = wceq 1540  wcel 2105  wne 2939  wrex 3069  Vcvv 3473  cdif 3945  cun 3946  cin 3947  wss 3948  {csn 4628  cotp 4636   class class class wbr 5148  {copab 5210   × cxp 5674  Predcpred 6299  cfv 6543  1st c1st 7977  2nd c2nd 7978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-ot 4637  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-pred 6300  df-iota 6495  df-fun 6545  df-fv 6551  df-1st 7979  df-2nd 7980
This theorem is referenced by:  sexp3  8144  xpord3inddlem  8145
  Copyright terms: Public domain W3C validator