Metamath Proof Explorer

Theorem xpord3pred

Description: Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 31-Jan-2025)

Ref Expression
Hypothesis xpord3.1 ⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑇 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
Assertion xpord3pred ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) ) ∖ { ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ } ) )

Proof

Step Hyp Ref Expression
1 xpord3.1 ⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑇 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
2 oteq1 ⊢ ( 𝑎 = 𝑋 → ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ = ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ )
3 predeq3 ⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ = ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ ) )
4 2 3 syl ⊢ ( 𝑎 = 𝑋 → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ ) )
5 predeq3 ⊢ ( 𝑎 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑎 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
6 sneq ⊢ ( 𝑎 = 𝑋 → { 𝑎 } = { 𝑋 } )
7 5 6 uneq12d ⊢ ( 𝑎 = 𝑋 → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) )
8 7 xpeq1d ⊢ ( 𝑎 = 𝑋 → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) = ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) )
9 8 xpeq1d ⊢ ( 𝑎 = 𝑋 → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) )
10 2 sneqd ⊢ ( 𝑎 = 𝑋 → { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ } )
11 9 10 difeq12d ⊢ ( 𝑎 = 𝑋 → ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ } ) )
12 4 11 eqeq12d ⊢ ( 𝑎 = 𝑋 → ( Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ↔ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ } ) ) )
13 oteq2 ⊢ ( 𝑏 = 𝑌 → ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ = ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ )
14 predeq3 ⊢ ( ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ = ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ ) )
15 13 14 syl ⊢ ( 𝑏 = 𝑌 → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ ) )
16 predeq3 ⊢ ( 𝑏 = 𝑌 → Pred ( 𝑆 , 𝐵 , 𝑏 ) = Pred ( 𝑆 , 𝐵 , 𝑌 ) )
17 sneq ⊢ ( 𝑏 = 𝑌 → { 𝑏 } = { 𝑌 } )
18 16 17 uneq12d ⊢ ( 𝑏 = 𝑌 → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) = ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) )
19 18 xpeq2d ⊢ ( 𝑏 = 𝑌 → ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) = ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) )
20 19 xpeq1d ⊢ ( 𝑏 = 𝑌 → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) )
21 13 sneqd ⊢ ( 𝑏 = 𝑌 → { ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ } = { ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ } )
22 20 21 difeq12d ⊢ ( 𝑏 = 𝑌 → ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ } ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ } ) )
23 15 22 eqeq12d ⊢ ( 𝑏 = 𝑌 → ( Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑋 , 𝑏 , 𝑐 ⟩ } ) ↔ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ } ) ) )
24 oteq3 ⊢ ( 𝑐 = 𝑍 → ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ )
25 predeq3 ⊢ ( ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ = ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) )
26 24 25 syl ⊢ ( 𝑐 = 𝑍 → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) )
27 predeq3 ⊢ ( 𝑐 = 𝑍 → Pred ( 𝑇 , 𝐶 , 𝑐 ) = Pred ( 𝑇 , 𝐶 , 𝑍 ) )
28 sneq ⊢ ( 𝑐 = 𝑍 → { 𝑐 } = { 𝑍 } )
29 27 28 uneq12d ⊢ ( 𝑐 = 𝑍 → ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) = ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) )
30 29 xpeq2d ⊢ ( 𝑐 = 𝑍 → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) ) )
31 24 sneqd ⊢ ( 𝑐 = 𝑍 → { ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ } = { ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ } )
32 30 31 difeq12d ⊢ ( 𝑐 = 𝑍 → ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ } ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) ) ∖ { ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ } ) )
33 26 32 eqeq12d ⊢ ( 𝑐 = 𝑍 → ( Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑋 , 𝑌 , 𝑐 ⟩ } ) ↔ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) ) ∖ { ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ } ) ) )
34 el2xptp ⊢ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ )
35 df-3an ⊢ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
36 simplrl ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → 𝑑 ∈ 𝐴 )
37 simplrr ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → 𝑒 ∈ 𝐵 )
38 simpr ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → 𝑓 ∈ 𝐶 )
39 36 37 38 3jca ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) )
40 simpll ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) )
41 39 40 jca ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) )
42 41 biantrurd ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
43 36 biantrurd ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( 𝑑 𝑅 𝑎 ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ) )
44 43 orbi1d ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ) )
45 37 biantrurd ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( 𝑒 𝑆 𝑏 ↔ ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ) )
46 45 orbi1d ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ↔ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) )
47 38 biantrurd ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( 𝑓 𝑇 𝑐 ↔ ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ) )
48 47 orbi1d ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ↔ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) )
49 44 46 48 3anbi123d ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ) )
50 49 anbi1d ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
51 42 50 bitr3d ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
52 35 51 bitrid ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
53 breq1 ⊢ ( 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
54 1 xpord3lem ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
55 53 54 bitrdi ⊢ ( 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
56 eleq1 ⊢ ( 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ↔ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) )
57 eldifsn ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ↔ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ≠ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
58 otelxp ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ↔ ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) )
59 elun ⊢ ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ↔ ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∨ 𝑑 ∈ { 𝑎 } ) )
60 vex ⊢ 𝑑 ∈ V
61 60 elpred ⊢ ( 𝑎 ∈ V → ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ) )
62 61 elv ⊢ ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) )
63 velsn ⊢ ( 𝑑 ∈ { 𝑎 } ↔ 𝑑 = 𝑎 )
64 62 63 orbi12i ⊢ ( ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∨ 𝑑 ∈ { 𝑎 } ) ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) )
65 59 64 bitri ⊢ ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) )
66 elun ⊢ ( 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ↔ ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∨ 𝑒 ∈ { 𝑏 } ) )
67 vex ⊢ 𝑒 ∈ V
68 67 elpred ⊢ ( 𝑏 ∈ V → ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ) )
69 68 elv ⊢ ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) )
70 velsn ⊢ ( 𝑒 ∈ { 𝑏 } ↔ 𝑒 = 𝑏 )
71 69 70 orbi12i ⊢ ( ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∨ 𝑒 ∈ { 𝑏 } ) ↔ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) )
72 66 71 bitri ⊢ ( 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ↔ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) )
73 elun ⊢ ( 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ↔ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ∨ 𝑓 ∈ { 𝑐 } ) )
74 vex ⊢ 𝑓 ∈ V
75 74 elpred ⊢ ( 𝑐 ∈ V → ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ↔ ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ) )
76 75 elv ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ↔ ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) )
77 velsn ⊢ ( 𝑓 ∈ { 𝑐 } ↔ 𝑓 = 𝑐 )
78 76 77 orbi12i ⊢ ( ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ∨ 𝑓 ∈ { 𝑐 } ) ↔ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) )
79 73 78 bitri ⊢ ( 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ↔ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) )
80 65 72 79 3anbi123i ⊢ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) )
81 58 80 bitri ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) )
82 60 67 74 otthne ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ≠ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
83 81 82 anbi12i ⊢ ( ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ≠ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
84 57 83 bitri ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
85 56 84 bitrdi ⊢ ( 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
86 55 85 bibi12d ⊢ ( 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( ( 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
87 52 86 syl5ibrcom ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) ) )
88 87 rexlimdva ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) → ( ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) ) )
89 88 rexlimdvva ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) ) )
90 34 89 biimtrid ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) ) )
91 90 pm5.32d ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) ) )
92 otex ⊢ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ V
93 vex ⊢ 𝑞 ∈ V
94 93 elpred ⊢ ( ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ∈ V → ( 𝑞 ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ) )
95 92 94 ax-mp ⊢ ( 𝑞 ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 𝑈 ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
96 elin ⊢ ( 𝑞 ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) )
97 91 95 96 3bitr4g ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ↔ 𝑞 ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) ) )
98 97 eqrdv ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) = ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) )
99 predss ⊢ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝐴
100 99 a1i ⊢ ( 𝑎 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝐴 )
101 snssi ⊢ ( 𝑎 ∈ 𝐴 → { 𝑎 } ⊆ 𝐴 )
102 100 101 unssd ⊢ ( 𝑎 ∈ 𝐴 → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ⊆ 𝐴 )
103 102 3ad2ant1 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ⊆ 𝐴 )
104 predss ⊢ Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ 𝐵
105 104 a1i ⊢ ( 𝑏 ∈ 𝐵 → Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ 𝐵 )
106 snssi ⊢ ( 𝑏 ∈ 𝐵 → { 𝑏 } ⊆ 𝐵 )
107 105 106 unssd ⊢ ( 𝑏 ∈ 𝐵 → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ⊆ 𝐵 )
108 107 3ad2ant2 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ⊆ 𝐵 )
109 xpss12 ⊢ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ⊆ 𝐴 ∧ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ⊆ 𝐵 ) → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ⊆ ( 𝐴 × 𝐵 ) )
110 103 108 109 syl2anc ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ⊆ ( 𝐴 × 𝐵 ) )
111 predss ⊢ Pred ( 𝑇 , 𝐶 , 𝑐 ) ⊆ 𝐶
112 111 a1i ⊢ ( 𝑐 ∈ 𝐶 → Pred ( 𝑇 , 𝐶 , 𝑐 ) ⊆ 𝐶 )
113 snssi ⊢ ( 𝑐 ∈ 𝐶 → { 𝑐 } ⊆ 𝐶 )
114 112 113 unssd ⊢ ( 𝑐 ∈ 𝐶 → ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ⊆ 𝐶 )
115 114 3ad2ant3 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ⊆ 𝐶 )
116 xpss12 ⊢ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ⊆ ( 𝐴 × 𝐵 ) ∧ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ⊆ 𝐶 ) → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
117 110 115 116 syl2anc ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
118 117 ssdifssd ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
119 sseqin2 ⊢ ( ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) )
120 118 119 sylib ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) )
121 98 120 eqtrd ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) )
122 12 23 33 121 vtocl3ga ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) ) ∖ { ⟨ 𝑋 , 𝑌 , 𝑍 ⟩ } ) )