Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  xpord3pred Structured version   Visualization version   GIF version

Theorem xpord3pred 33414
Description: Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 21-Aug-2024.)
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 opeq1 4760 . . . . 5 (𝑎 = 𝑋 → ⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩)
21opeq1d 4768 . . . 4 (𝑎 = 𝑋 → ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑏⟩, 𝑐⟩)
3 predeq3 6134 . . . 4 (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑏⟩, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩))
42, 3syl 17 . . 3 (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩))
5 predeq3 6134 . . . . . . 7 (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
6 sneq 4527 . . . . . . 7 (𝑎 = 𝑋 → {𝑎} = {𝑋})
75, 6uneq12d 4055 . . . . . 6 (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
87xpeq1d 5555 . . . . 5 (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
98xpeq1d 5555 . . . 4 (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
102sneqd 4529 . . . 4 (𝑎 = 𝑋 → {⟨⟨𝑎, 𝑏⟩, 𝑐⟩} = {⟨⟨𝑋, 𝑏⟩, 𝑐⟩})
119, 10difeq12d 4015 . . 3 (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑏⟩, 𝑐⟩}))
124, 11eqeq12d 2755 . 2 (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑏⟩, 𝑐⟩})))
13 opeq2 4762 . . . . 5 (𝑏 = 𝑌 → ⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩)
1413opeq1d 4768 . . . 4 (𝑏 = 𝑌 → ⟨⟨𝑋, 𝑏⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑌⟩, 𝑐⟩)
15 predeq3 6134 . . . 4 (⟨⟨𝑋, 𝑏⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑌⟩, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩))
1614, 15syl 17 . . 3 (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩))
17 predeq3 6134 . . . . . . 7 (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
18 sneq 4527 . . . . . . 7 (𝑏 = 𝑌 → {𝑏} = {𝑌})
1917, 18uneq12d 4055 . . . . . 6 (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
2019xpeq2d 5556 . . . . 5 (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
2120xpeq1d 5555 . . . 4 (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
2214sneqd 4529 . . . 4 (𝑏 = 𝑌 → {⟨⟨𝑋, 𝑏⟩, 𝑐⟩} = {⟨⟨𝑋, 𝑌⟩, 𝑐⟩})
2321, 22difeq12d 4015 . . 3 (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑏⟩, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑐⟩}))
2416, 23eqeq12d 2755 . 2 (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑏⟩, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑐⟩})))
25 opeq2 4762 . . . 4 (𝑐 = 𝑍 → ⟨⟨𝑋, 𝑌⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑌⟩, 𝑍⟩)
26 predeq3 6134 . . . 4 (⟨⟨𝑋, 𝑌⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑌⟩, 𝑍⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑍⟩))
2725, 26syl 17 . . 3 (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑍⟩))
28 predeq3 6134 . . . . . 6 (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍))
29 sneq 4527 . . . . . 6 (𝑐 = 𝑍 → {𝑐} = {𝑍})
3028, 29uneq12d 4055 . . . . 5 (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))
3130xpeq2d 5556 . . . 4 (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})))
3225sneqd 4529 . . . 4 (𝑐 = 𝑍 → {⟨⟨𝑋, 𝑌⟩, 𝑐⟩} = {⟨⟨𝑋, 𝑌⟩, 𝑍⟩})
3331, 32difeq12d 4015 . . 3 (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑍⟩}))
3427, 33eqeq12d 2755 . 2 (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑍⟩})))
35 elxpxp 33260 . . . . . . 7 (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)
36 df-3an 1090 . . . . . . . . . . 11 ((𝑑𝐴𝑒𝐵𝑓𝐶) ↔ ((𝑑𝐴𝑒𝐵) ∧ 𝑓𝐶))
37 df-3an 1090 . . . . . . . . . . . . 13 (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
38 eldif 3854 . . . . . . . . . . . . . . . 16 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
39 opelxp 5562 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (⟨𝑑, 𝑒⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
40 opelxp 5562 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑑, 𝑒⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
41 elun 4040 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}))
42 vex 3403 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑑 ∈ V
4342elpred 6143 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎)))
4443elv 3405 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎))
45 velsn 4533 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎)
4644, 45orbi12i 914 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
4741, 46bitri 278 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
48 elun 4040 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}))
49 vex 3403 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑒 ∈ V
5049elpred 6143 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏)))
5150elv 3405 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏))
52 velsn 4533 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏)
5351, 52orbi12i 914 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
5448, 53bitri 278 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
5547, 54anbi12i 630 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
5640, 55bitri 278 . . . . . . . . . . . . . . . . . . 19 (⟨𝑑, 𝑒⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
57 elun 4040 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}))
58 vex 3403 . . . . . . . . . . . . . . . . . . . . . . 23 𝑓 ∈ V
5958elpred 6143 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐)))
6059elv 3405 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐))
61 velsn 4533 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐)
6260, 61orbi12i 914 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
6357, 62bitri 278 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
6456, 63anbi12i 630 . . . . . . . . . . . . . . . . . 18 ((⟨𝑑, 𝑒⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
6539, 64bitri 278 . . . . . . . . . . . . . . . . 17 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
66 df-ne 2936 . . . . . . . . . . . . . . . . . . 19 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
6742, 49, 58otthne 33259 . . . . . . . . . . . . . . . . . . 19 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
6866, 67bitr3i 280 . . . . . . . . . . . . . . . . . 18 (¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
69 opex 5323 . . . . . . . . . . . . . . . . . . 19 ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ V
7069elsn 4532 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩} ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
7168, 70xchnxbir 336 . . . . . . . . . . . . . . . . 17 (¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩} ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
7265, 71anbi12i 630 . . . . . . . . . . . . . . . 16 ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
7338, 72bitri 278 . . . . . . . . . . . . . . 15 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
74 simpr1 1195 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → 𝑑𝐴)
7574biantrurd 536 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (𝑑𝑅𝑎 ↔ (𝑑𝐴𝑑𝑅𝑎)))
7675orbi1d 916 . . . . . . . . . . . . . . . . . 18 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((𝑑𝑅𝑎𝑑 = 𝑎) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)))
77 simpr2 1196 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → 𝑒𝐵)
7877biantrurd 536 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (𝑒𝑆𝑏 ↔ (𝑒𝐵𝑒𝑆𝑏)))
7978orbi1d 916 . . . . . . . . . . . . . . . . . 18 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((𝑒𝑆𝑏𝑒 = 𝑏) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
80 simpr3 1197 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → 𝑓𝐶)
8180biantrurd 536 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (𝑓𝑇𝑐 ↔ (𝑓𝐶𝑓𝑇𝑐)))
8281orbi1d 916 . . . . . . . . . . . . . . . . . 18 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((𝑓𝑇𝑐𝑓 = 𝑐) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
8376, 79, 823anbi123d 1437 . . . . . . . . . . . . . . . . 17 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
84 df-3an 1090 . . . . . . . . . . . . . . . . 17 ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
8583, 84bitrdi 290 . . . . . . . . . . . . . . . 16 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
8685anbi1d 633 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) ↔ (((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
8773, 86bitr4id 293 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
88 pm3.22 463 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)))
8988biantrurd 536 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
9087, 89bitr2d 283 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
9137, 90syl5bb 286 . . . . . . . . . . . 12 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
92 breq1 5034 . . . . . . . . . . . . . 14 (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
93 xpord3.1 . . . . . . . . . . . . . . 15 𝑈 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑦 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ ((((1st ‘(1st𝑥))𝑅(1st ‘(1st𝑦)) ∨ (1st ‘(1st𝑥)) = (1st ‘(1st𝑦))) ∧ ((2nd ‘(1st𝑥))𝑆(2nd ‘(1st𝑦)) ∨ (2nd ‘(1st𝑥)) = (2nd ‘(1st𝑦))) ∧ ((2nd𝑥)𝑇(2nd𝑦) ∨ (2nd𝑥) = (2nd𝑦))) ∧ 𝑥𝑦))}
9493xpord3lem 33411 . . . . . . . . . . . . . 14 (⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
9592, 94bitrdi 290 . . . . . . . . . . . . 13 (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
96 eleq1 2821 . . . . . . . . . . . . 13 (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
9795, 96bibi12d 349 . . . . . . . . . . . 12 (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
9891, 97syl5ibrcom 250 . . . . . . . . . . 11 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
9936, 98sylan2br 598 . . . . . . . . . 10 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ ((𝑑𝐴𝑒𝐵) ∧ 𝑓𝐶)) → (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
10099anassrs 471 . . . . . . . . 9 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
101100rexlimdva 3195 . . . . . . . 8 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) → (∃𝑓𝐶 𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
102101rexlimdvva 3205 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
10335, 102syl5bi 245 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
104103pm5.32d 580 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
105 opex 5323 . . . . . 6 ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ V
106 vex 3403 . . . . . . 7 𝑞 ∈ V
107106elpred 6143 . . . . . 6 (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩)))
108105, 107ax-mp 5 . . . . 5 (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
109 elin 3860 . . . . 5 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
110104, 108, 1093bitr4g 317 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
111110eqrdv 2737 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
112 predss 6137 . . . . . . . . . 10 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
113112a1i 11 . . . . . . . . 9 (𝑎𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
114 snssi 4697 . . . . . . . . 9 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
115113, 114unssd 4077 . . . . . . . 8 (𝑎𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
1161153ad2ant1 1134 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
117 predss 6137 . . . . . . . . . 10 Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
118117a1i 11 . . . . . . . . 9 (𝑏𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
119 snssi 4697 . . . . . . . . 9 (𝑏𝐵 → {𝑏} ⊆ 𝐵)
120118, 119unssd 4077 . . . . . . . 8 (𝑏𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
1211203ad2ant2 1135 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
122 xpss12 5541 . . . . . . 7 (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
123116, 121, 122syl2anc 587 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
124 predss 6137 . . . . . . . . 9 Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶
125124a1i 11 . . . . . . . 8 (𝑐𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶)
126 snssi 4697 . . . . . . . 8 (𝑐𝐶 → {𝑐} ⊆ 𝐶)
127125, 126unssd 4077 . . . . . . 7 (𝑐𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
1281273ad2ant3 1136 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
129 xpss12 5541 . . . . . 6 ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
130123, 128, 129syl2anc 587 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
131130ssdifssd 4034 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶))
132 sseqin2 4107 . . . 4 (((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
133131, 132sylib 221 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
134111, 133eqtrd 2774 . 2 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
13512, 24, 34, 134vtocl3ga 3483 1 ((𝑋𝐴𝑌𝐵𝑍𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑍⟩}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 846  w3o 1087  w3a 1088   = wceq 1542  wcel 2114  wne 2935  wrex 3055  Vcvv 3399  cdif 3841  cun 3842  cin 3843  wss 3844  {csn 4517  cop 4523   class class class wbr 5031  {copab 5093   × cxp 5524  Predcpred 6129  cfv 6340  1st c1st 7715  2nd c2nd 7716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5168  ax-nul 5175  ax-pr 5297  ax-un 7482
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ne 2936  df-ral 3059  df-rex 3060  df-rab 3063  df-v 3401  df-sbc 3682  df-csb 3792  df-dif 3847  df-un 3849  df-in 3851  df-ss 3861  df-nul 4213  df-if 4416  df-sn 4518  df-pr 4520  df-op 4524  df-uni 4798  df-iun 4884  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5430  df-xp 5532  df-rel 5533  df-cnv 5534  df-co 5535  df-dm 5536  df-rn 5537  df-res 5538  df-ima 5539  df-pred 6130  df-iota 6298  df-fun 6342  df-fv 6348  df-1st 7717  df-2nd 7718
This theorem is referenced by:  sexp3  33415  xpord3ind  33416
  Copyright terms: Public domain W3C validator