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 33807
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 4805 . . . . 5 (𝑎 = 𝑋 → ⟨𝑎, 𝑏⟩ = ⟨𝑋, 𝑏⟩)
21opeq1d 4811 . . . 4 (𝑎 = 𝑋 → ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑏⟩, 𝑐⟩)
3 predeq3 6210 . . . 4 (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑏⟩, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩))
42, 3syl 17 . . 3 (𝑎 = 𝑋 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩))
5 predeq3 6210 . . . . . . 7 (𝑎 = 𝑋 → Pred(𝑅, 𝐴, 𝑎) = Pred(𝑅, 𝐴, 𝑋))
6 sneq 4572 . . . . . . 7 (𝑎 = 𝑋 → {𝑎} = {𝑋})
75, 6uneq12d 4099 . . . . . 6 (𝑎 = 𝑋 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) = (Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}))
87xpeq1d 5619 . . . . 5 (𝑎 = 𝑋 → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
98xpeq1d 5619 . . . 4 (𝑎 = 𝑋 → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
102sneqd 4574 . . . 4 (𝑎 = 𝑋 → {⟨⟨𝑎, 𝑏⟩, 𝑐⟩} = {⟨⟨𝑋, 𝑏⟩, 𝑐⟩})
119, 10difeq12d 4059 . . 3 (𝑎 = 𝑋 → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑏⟩, 𝑐⟩}))
124, 11eqeq12d 2755 . 2 (𝑎 = 𝑋 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑏⟩, 𝑐⟩})))
13 opeq2 4806 . . . . 5 (𝑏 = 𝑌 → ⟨𝑋, 𝑏⟩ = ⟨𝑋, 𝑌⟩)
1413opeq1d 4811 . . . 4 (𝑏 = 𝑌 → ⟨⟨𝑋, 𝑏⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑌⟩, 𝑐⟩)
15 predeq3 6210 . . . 4 (⟨⟨𝑋, 𝑏⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑌⟩, 𝑐⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩))
1614, 15syl 17 . . 3 (𝑏 = 𝑌 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩))
17 predeq3 6210 . . . . . . 7 (𝑏 = 𝑌 → Pred(𝑆, 𝐵, 𝑏) = Pred(𝑆, 𝐵, 𝑌))
18 sneq 4572 . . . . . . 7 (𝑏 = 𝑌 → {𝑏} = {𝑌})
1917, 18uneq12d 4099 . . . . . 6 (𝑏 = 𝑌 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) = (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌}))
2019xpeq2d 5620 . . . . 5 (𝑏 = 𝑌 → ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) = ((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})))
2120xpeq1d 5619 . . . 4 (𝑏 = 𝑌 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
2214sneqd 4574 . . . 4 (𝑏 = 𝑌 → {⟨⟨𝑋, 𝑏⟩, 𝑐⟩} = {⟨⟨𝑋, 𝑌⟩, 𝑐⟩})
2321, 22difeq12d 4059 . . 3 (𝑏 = 𝑌 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑏⟩, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑐⟩}))
2416, 23eqeq12d 2755 . 2 (𝑏 = 𝑌 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑏⟩, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑐⟩})))
25 opeq2 4806 . . . 4 (𝑐 = 𝑍 → ⟨⟨𝑋, 𝑌⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑌⟩, 𝑍⟩)
26 predeq3 6210 . . . 4 (⟨⟨𝑋, 𝑌⟩, 𝑐⟩ = ⟨⟨𝑋, 𝑌⟩, 𝑍⟩ → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑍⟩))
2725, 26syl 17 . . 3 (𝑐 = 𝑍 → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩) = Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑍⟩))
28 predeq3 6210 . . . . . 6 (𝑐 = 𝑍 → Pred(𝑇, 𝐶, 𝑐) = Pred(𝑇, 𝐶, 𝑍))
29 sneq 4572 . . . . . 6 (𝑐 = 𝑍 → {𝑐} = {𝑍})
3028, 29uneq12d 4099 . . . . 5 (𝑐 = 𝑍 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) = (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍}))
3130xpeq2d 5620 . . . 4 (𝑐 = 𝑍 → (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) = (((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})))
3225sneqd 4574 . . . 4 (𝑐 = 𝑍 → {⟨⟨𝑋, 𝑌⟩, 𝑐⟩} = {⟨⟨𝑋, 𝑌⟩, 𝑍⟩})
3331, 32difeq12d 4059 . . 3 (𝑐 = 𝑍 → ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑐⟩}) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑍⟩}))
3427, 33eqeq12d 2755 . 2 (𝑐 = 𝑍 → (Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑐⟩}) ↔ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑍⟩})))
35 elxpxp 33692 . . . . . . 7 (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ↔ ∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩)
36 df-3an 1088 . . . . . . . . . . 11 ((𝑑𝐴𝑒𝐵𝑓𝐶) ↔ ((𝑑𝐴𝑒𝐵) ∧ 𝑓𝐶))
37 df-3an 1088 . . . . . . . . . . . . 13 (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
38 eldif 3898 . . . . . . . . . . . . . . . 16 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
39 opelxp 5626 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ (⟨𝑑, 𝑒⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})))
40 opelxp 5626 . . . . . . . . . . . . . . . . . . . 20 (⟨𝑑, 𝑒⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})))
41 elun 4084 . . . . . . . . . . . . . . . . . . . . . 22 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}))
42 vex 3437 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑑 ∈ V
4342elpred 6223 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑎 ∈ V → (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎)))
4443elv 3439 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ↔ (𝑑𝐴𝑑𝑅𝑎))
45 velsn 4578 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑑 ∈ {𝑎} ↔ 𝑑 = 𝑎)
4644, 45orbi12i 912 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑑 ∈ Pred(𝑅, 𝐴, 𝑎) ∨ 𝑑 ∈ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
4741, 46bitri 274 . . . . . . . . . . . . . . . . . . . . 21 (𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎))
48 elun 4084 . . . . . . . . . . . . . . . . . . . . . 22 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}))
49 vex 3437 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑒 ∈ V
5049elpred 6223 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑏 ∈ V → (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏)))
5150elv 3439 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ↔ (𝑒𝐵𝑒𝑆𝑏))
52 velsn 4578 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑒 ∈ {𝑏} ↔ 𝑒 = 𝑏)
5351, 52orbi12i 912 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑒 ∈ Pred(𝑆, 𝐵, 𝑏) ∨ 𝑒 ∈ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
5448, 53bitri 274 . . . . . . . . . . . . . . . . . . . . 21 (𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏))
5547, 54anbi12i 627 . . . . . . . . . . . . . . . . . . . 20 ((𝑑 ∈ (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ∧ 𝑒 ∈ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
5640, 55bitri 274 . . . . . . . . . . . . . . . . . . 19 (⟨𝑑, 𝑒⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
57 elun 4084 . . . . . . . . . . . . . . . . . . . 20 (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}))
58 vex 3437 . . . . . . . . . . . . . . . . . . . . . . 23 𝑓 ∈ V
5958elpred 6223 . . . . . . . . . . . . . . . . . . . . . 22 (𝑐 ∈ V → (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐)))
6059elv 3439 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ↔ (𝑓𝐶𝑓𝑇𝑐))
61 velsn 4578 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ {𝑐} ↔ 𝑓 = 𝑐)
6260, 61orbi12i 912 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 ∈ Pred(𝑇, 𝐶, 𝑐) ∨ 𝑓 ∈ {𝑐}) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
6357, 62bitri 274 . . . . . . . . . . . . . . . . . . 19 (𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))
6456, 63anbi12i 627 . . . . . . . . . . . . . . . . . 18 ((⟨𝑑, 𝑒⟩ ∈ ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ∧ 𝑓 ∈ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
6539, 64bitri 274 . . . . . . . . . . . . . . . . 17 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
66 df-ne 2945 . . . . . . . . . . . . . . . . . . 19 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
6742, 49, 58otthne 33691 . . . . . . . . . . . . . . . . . . 19 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ≠ ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
6866, 67bitr3i 276 . . . . . . . . . . . . . . . . . 18 (¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
69 opex 5380 . . . . . . . . . . . . . . . . . . 19 ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ V
7069elsn 4577 . . . . . . . . . . . . . . . . . 18 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩} ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ = ⟨⟨𝑎, 𝑏⟩, 𝑐⟩)
7168, 70xchnxbir 333 . . . . . . . . . . . . . . . . 17 (¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩} ↔ (𝑑𝑎𝑒𝑏𝑓𝑐))
7265, 71anbi12i 627 . . . . . . . . . . . . . . . 16 ((⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∧ ¬ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
7338, 72bitri 274 . . . . . . . . . . . . . . 15 (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))
74 simpr1 1193 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → 𝑑𝐴)
7574biantrurd 533 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (𝑑𝑅𝑎 ↔ (𝑑𝐴𝑑𝑅𝑎)))
7675orbi1d 914 . . . . . . . . . . . . . . . . . 18 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((𝑑𝑅𝑎𝑑 = 𝑎) ↔ ((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎)))
77 simpr2 1194 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → 𝑒𝐵)
7877biantrurd 533 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (𝑒𝑆𝑏 ↔ (𝑒𝐵𝑒𝑆𝑏)))
7978orbi1d 914 . . . . . . . . . . . . . . . . . 18 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((𝑒𝑆𝑏𝑒 = 𝑏) ↔ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)))
80 simpr3 1195 . . . . . . . . . . . . . . . . . . . 20 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → 𝑓𝐶)
8180biantrurd 533 . . . . . . . . . . . . . . . . . . 19 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (𝑓𝑇𝑐 ↔ (𝑓𝐶𝑓𝑇𝑐)))
8281orbi1d 914 . . . . . . . . . . . . . . . . . 18 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((𝑓𝑇𝑐𝑓 = 𝑐) ↔ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
8376, 79, 823anbi123d 1435 . . . . . . . . . . . . . . . . 17 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ↔ (((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
84 df-3an 1088 . . . . . . . . . . . . . . . . 17 ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)))
8583, 84bitrdi 287 . . . . . . . . . . . . . . . 16 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ↔ ((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐))))
8685anbi1d 630 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) ↔ (((((𝑑𝐴𝑑𝑅𝑎) ∨ 𝑑 = 𝑎) ∧ ((𝑒𝐵𝑒𝑆𝑏) ∨ 𝑒 = 𝑏)) ∧ ((𝑓𝐶𝑓𝑇𝑐) ∨ 𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
8773, 86bitr4id 290 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
88 pm3.22 460 . . . . . . . . . . . . . . 15 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)))
8988biantrurd 533 . . . . . . . . . . . . . 14 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
9087, 89bitr2d 279 . . . . . . . . . . . . 13 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → ((((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶)) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
9137, 90syl5bb 283 . . . . . . . . . . . 12 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
92 breq1 5078 . . . . . . . . . . . . . 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 33804 . . . . . . . . . . . . . 14 (⟨⟨𝑑, 𝑒⟩, 𝑓𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))))
9592, 94bitrdi 287 . . . . . . . . . . . . 13 (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ ((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐)))))
96 eleq1 2827 . . . . . . . . . . . . 13 (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
9795, 96bibi12d 346 . . . . . . . . . . . 12 (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → ((𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})) ↔ (((𝑑𝐴𝑒𝐵𝑓𝐶) ∧ (𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (((𝑑𝑅𝑎𝑑 = 𝑎) ∧ (𝑒𝑆𝑏𝑒 = 𝑏) ∧ (𝑓𝑇𝑐𝑓 = 𝑐)) ∧ (𝑑𝑎𝑒𝑏𝑓𝑐))) ↔ ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
9891, 97syl5ibrcom 246 . . . . . . . . . . 11 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵𝑓𝐶)) → (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
9936, 98sylan2br 595 . . . . . . . . . 10 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ ((𝑑𝐴𝑒𝐵) ∧ 𝑓𝐶)) → (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
10099anassrs 468 . . . . . . . . 9 ((((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) ∧ 𝑓𝐶) → (𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
101100rexlimdva 3214 . . . . . . . 8 (((𝑎𝐴𝑏𝐵𝑐𝐶) ∧ (𝑑𝐴𝑒𝐵)) → (∃𝑓𝐶 𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
102101rexlimdvva 3224 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (∃𝑑𝐴𝑒𝐵𝑓𝐶 𝑞 = ⟨⟨𝑑, 𝑒⟩, 𝑓⟩ → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
10335, 102syl5bi 241 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) → (𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ↔ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
104103pm5.32d 577 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
105 opex 5380 . . . . . 6 ⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ V
106 vex 3437 . . . . . . 7 𝑞 ∈ V
107106elpred 6223 . . . . . 6 (⟨⟨𝑎, 𝑏⟩, 𝑐⟩ ∈ V → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩)))
108105, 107ax-mp 5 . . . . 5 (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞𝑈⟨⟨𝑎, 𝑏⟩, 𝑐⟩))
109 elin 3904 . . . . 5 (𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})) ↔ (𝑞 ∈ ((𝐴 × 𝐵) × 𝐶) ∧ 𝑞 ∈ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
110104, 108, 1093bitr4g 314 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (𝑞 ∈ Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) ↔ 𝑞 ∈ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))))
111110eqrdv 2737 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})))
112 predss 6214 . . . . . . . . . 10 Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴
113112a1i 11 . . . . . . . . 9 (𝑎𝐴 → Pred(𝑅, 𝐴, 𝑎) ⊆ 𝐴)
114 snssi 4742 . . . . . . . . 9 (𝑎𝐴 → {𝑎} ⊆ 𝐴)
115113, 114unssd 4121 . . . . . . . 8 (𝑎𝐴 → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
1161153ad2ant1 1132 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴)
117 predss 6214 . . . . . . . . . 10 Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵
118117a1i 11 . . . . . . . . 9 (𝑏𝐵 → Pred(𝑆, 𝐵, 𝑏) ⊆ 𝐵)
119 snssi 4742 . . . . . . . . 9 (𝑏𝐵 → {𝑏} ⊆ 𝐵)
120118, 119unssd 4121 . . . . . . . 8 (𝑏𝐵 → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
1211203ad2ant2 1133 . . . . . . 7 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵)
122 xpss12 5605 . . . . . . 7 (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) ⊆ 𝐴 ∧ (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏}) ⊆ 𝐵) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
123116, 121, 122syl2anc 584 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵))
124 predss 6214 . . . . . . . . 9 Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶
125124a1i 11 . . . . . . . 8 (𝑐𝐶 → Pred(𝑇, 𝐶, 𝑐) ⊆ 𝐶)
126 snssi 4742 . . . . . . . 8 (𝑐𝐶 → {𝑐} ⊆ 𝐶)
127125, 126unssd 4121 . . . . . . 7 (𝑐𝐶 → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
1281273ad2ant3 1134 . . . . . 6 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶)
129 xpss12 5605 . . . . . 6 ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) ⊆ (𝐴 × 𝐵) ∧ (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐}) ⊆ 𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
130123, 128, 129syl2anc 584 . . . . 5 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ⊆ ((𝐴 × 𝐵) × 𝐶))
131130ssdifssd 4078 . . . 4 ((𝑎𝐴𝑏𝐵𝑐𝐶) → ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶))
132 sseqin2 4150 . . . 4 (((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}) ⊆ ((𝐴 × 𝐵) × 𝐶) ↔ (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
133131, 132sylib 217 . . 3 ((𝑎𝐴𝑏𝐵𝑐𝐶) → (((𝐴 × 𝐵) × 𝐶) ∩ ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩})) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
134111, 133eqtrd 2779 . 2 ((𝑎𝐴𝑏𝐵𝑐𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑎, 𝑏⟩, 𝑐⟩) = ((((Pred(𝑅, 𝐴, 𝑎) ∪ {𝑎}) × (Pred(𝑆, 𝐵, 𝑏) ∪ {𝑏})) × (Pred(𝑇, 𝐶, 𝑐) ∪ {𝑐})) ∖ {⟨⟨𝑎, 𝑏⟩, 𝑐⟩}))
13512, 24, 34, 134vtocl3ga 3518 1 ((𝑋𝐴𝑌𝐵𝑍𝐶) → Pred(𝑈, ((𝐴 × 𝐵) × 𝐶), ⟨⟨𝑋, 𝑌⟩, 𝑍⟩) = ((((Pred(𝑅, 𝐴, 𝑋) ∪ {𝑋}) × (Pred(𝑆, 𝐵, 𝑌) ∪ {𝑌})) × (Pred(𝑇, 𝐶, 𝑍) ∪ {𝑍})) ∖ {⟨⟨𝑋, 𝑌⟩, 𝑍⟩}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 844  w3o 1085  w3a 1086   = wceq 1539  wcel 2107  wne 2944  wrex 3066  Vcvv 3433  cdif 3885  cun 3886  cin 3887  wss 3888  {csn 4562  cop 4568   class class class wbr 5075  {copab 5137   × cxp 5588  Predcpred 6205  cfv 6437  1st c1st 7838  2nd c2nd 7839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353  ax-un 7597
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-sbc 3718  df-csb 3834  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-iun 4927  df-br 5076  df-opab 5138  df-mpt 5159  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-pred 6206  df-iota 6395  df-fun 6439  df-fv 6445  df-1st 7840  df-2nd 7841
This theorem is referenced by:  sexp3  33808  xpord3ind  33809
  Copyright terms: Public domain W3C validator