Metamath Proof Explorer

Theorem xpord3pred

Description: Calculate the predecsessor class for the triple order. (Contributed by Scott Fenton, 21-Aug-2024)

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 opeq1 ⊢ ( 𝑎 = 𝑋 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑋 , 𝑏 ⟩ )
3 2 opeq1d ⊢ ( 𝑎 = 𝑋 → ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ = ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ )
4 predeq3 ⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ = ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ ) )
5 3 4 syl ⊢ ( 𝑎 = 𝑋 → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ ) )
6 predeq3 ⊢ ( 𝑎 = 𝑋 → Pred ( 𝑅 , 𝐴 , 𝑎 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
7 sneq ⊢ ( 𝑎 = 𝑋 → { 𝑎 } = { 𝑋 } )
8 6 7 uneq12d ⊢ ( 𝑎 = 𝑋 → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) = ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) )
9 8 xpeq1d ⊢ ( 𝑎 = 𝑋 → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) = ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) )
10 9 xpeq1d ⊢ ( 𝑎 = 𝑋 → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) )
11 3 sneqd ⊢ ( 𝑎 = 𝑋 → { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } = { ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ } )
12 10 11 difeq12d ⊢ ( 𝑎 = 𝑋 → ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ } ) )
13 5 12 eqeq12d ⊢ ( 𝑎 = 𝑋 → ( Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ↔ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) )
14 opeq2 ⊢ ( 𝑏 = 𝑌 → ⟨ 𝑋 , 𝑏 ⟩ = ⟨ 𝑋 , 𝑌 ⟩ )
15 14 opeq1d ⊢ ( 𝑏 = 𝑌 → ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ )
16 predeq3 ⊢ ( ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ ) )
17 15 16 syl ⊢ ( 𝑏 = 𝑌 → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ ) )
18 predeq3 ⊢ ( 𝑏 = 𝑌 → Pred ( 𝑆 , 𝐵 , 𝑏 ) = Pred ( 𝑆 , 𝐵 , 𝑌 ) )
19 sneq ⊢ ( 𝑏 = 𝑌 → { 𝑏 } = { 𝑌 } )
20 18 19 uneq12d ⊢ ( 𝑏 = 𝑌 → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) = ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) )
21 20 xpeq2d ⊢ ( 𝑏 = 𝑌 → ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) = ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) )
22 21 xpeq1d ⊢ ( 𝑏 = 𝑌 → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) )
23 15 sneqd ⊢ ( 𝑏 = 𝑌 → { ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ } = { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ } )
24 22 23 difeq12d ⊢ ( 𝑏 = 𝑌 → ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ } ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ } ) )
25 17 24 eqeq12d ⊢ ( 𝑏 = 𝑌 → ( Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑏 ⟩ , 𝑐 ⟩ } ) ↔ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ } ) ) )
26 opeq2 ⊢ ( 𝑐 = 𝑍 → ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ )
27 predeq3 ⊢ ( ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ = ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ) )
28 26 27 syl ⊢ ( 𝑐 = 𝑍 → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ ) = Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ) )
29 predeq3 ⊢ ( 𝑐 = 𝑍 → Pred ( 𝑇 , 𝐶 , 𝑐 ) = Pred ( 𝑇 , 𝐶 , 𝑍 ) )
30 sneq ⊢ ( 𝑐 = 𝑍 → { 𝑐 } = { 𝑍 } )
31 29 30 uneq12d ⊢ ( 𝑐 = 𝑍 → ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) = ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) )
32 31 xpeq2d ⊢ ( 𝑐 = 𝑍 → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) = ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) ) )
33 26 sneqd ⊢ ( 𝑐 = 𝑍 → { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ } = { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ } )
34 32 33 difeq12d ⊢ ( 𝑐 = 𝑍 → ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ } ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ } ) )
35 28 34 eqeq12d ⊢ ( 𝑐 = 𝑍 → ( Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑐 ⟩ } ) ↔ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ } ) ) )
36 elxpxp ⊢ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ )
37 df-3an ⊢ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐶 ) )
38 df-3an ⊢ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
39 eldif ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ↔ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ¬ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) )
40 opelxp ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ↔ ( ⟨ 𝑑 , 𝑒 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) )
41 opelxp ⊢ ( ⟨ 𝑑 , 𝑒 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ↔ ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) )
42 elun ⊢ ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ↔ ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∨ 𝑑 ∈ { 𝑎 } ) )
43 vex ⊢ 𝑑 ∈ V
44 43 elpred ⊢ ( 𝑎 ∈ V → ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ) )
45 44 elv ⊢ ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) )
46 velsn ⊢ ( 𝑑 ∈ { 𝑎 } ↔ 𝑑 = 𝑎 )
47 45 46 orbi12i ⊢ ( ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∨ 𝑑 ∈ { 𝑎 } ) ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) )
48 42 47 bitri ⊢ ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) )
49 elun ⊢ ( 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ↔ ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∨ 𝑒 ∈ { 𝑏 } ) )
50 vex ⊢ 𝑒 ∈ V
51 50 elpred ⊢ ( 𝑏 ∈ V → ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ) )
52 51 elv ⊢ ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) )
53 velsn ⊢ ( 𝑒 ∈ { 𝑏 } ↔ 𝑒 = 𝑏 )
54 52 53 orbi12i ⊢ ( ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∨ 𝑒 ∈ { 𝑏 } ) ↔ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) )
55 49 54 bitri ⊢ ( 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ↔ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) )
56 48 55 anbi12i ⊢ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) )
57 41 56 bitri ⊢ ( ⟨ 𝑑 , 𝑒 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) )
58 elun ⊢ ( 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ↔ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ∨ 𝑓 ∈ { 𝑐 } ) )
59 vex ⊢ 𝑓 ∈ V
60 59 elpred ⊢ ( 𝑐 ∈ V → ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ↔ ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ) )
61 60 elv ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ↔ ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) )
62 velsn ⊢ ( 𝑓 ∈ { 𝑐 } ↔ 𝑓 = 𝑐 )
63 61 62 orbi12i ⊢ ( ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ∨ 𝑓 ∈ { 𝑐 } ) ↔ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) )
64 58 63 bitri ⊢ ( 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ↔ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) )
65 57 64 anbi12i ⊢ ( ( ⟨ 𝑑 , 𝑒 ⟩ ∈ ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) )
66 40 65 bitri ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) )
67 df-ne ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ≠ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ ¬ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ )
68 43 50 59 otthne ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ≠ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
69 67 68 bitr3i ⊢ ( ¬ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
70 opex ⊢ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ V
71 70 elsn ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ = ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ )
72 69 71 xchnxbir ⊢ ( ¬ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
73 66 72 anbi12i ⊢ ( ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ¬ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ↔ ( ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
74 39 73 bitri ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ↔ ( ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
75 simpr1 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → 𝑑 ∈ 𝐴 )
76 75 biantrurd ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( 𝑑 𝑅 𝑎 ↔ ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ) )
77 76 orbi1d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ) )
78 simpr2 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → 𝑒 ∈ 𝐵 )
79 78 biantrurd ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( 𝑒 𝑆 𝑏 ↔ ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ) )
80 79 orbi1d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ↔ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) )
81 simpr3 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → 𝑓 ∈ 𝐶 )
82 81 biantrurd ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( 𝑓 𝑇 𝑐 ↔ ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ) )
83 82 orbi1d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ↔ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) )
84 77 80 83 3anbi123d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ) )
85 df-3an ⊢ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) )
86 84 85 bitrdi ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ↔ ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ) )
87 86 anbi1d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑑 𝑅 𝑎 ) ∨ 𝑑 = 𝑎 ) ∧ ( ( 𝑒 ∈ 𝐵 ∧ 𝑒 𝑆 𝑏 ) ∨ 𝑒 = 𝑏 ) ) ∧ ( ( 𝑓 ∈ 𝐶 ∧ 𝑓 𝑇 𝑐 ) ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
88 74 87 bitr4id ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ↔ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
89 pm3.22 ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) )
90 89 biantrurd ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
91 88 90 bitr2d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) )
92 38 91 syl5bb ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) )
93 breq1 ⊢ ( 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) )
94 1 xpord3lem ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) )
95 93 94 bitrdi ⊢ ( 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ) )
96 eleq1 ⊢ ( 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) )
97 95 96 bibi12d ⊢ ( 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( ( 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ↔ ( ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( ( 𝑑 𝑅 𝑎 ∨ 𝑑 = 𝑎 ) ∧ ( 𝑒 𝑆 𝑏 ∨ 𝑒 = 𝑏 ) ∧ ( 𝑓 𝑇 𝑐 ∨ 𝑓 = 𝑐 ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) ) ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ) )
98 92 97 syl5ibrcom ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ∧ 𝑓 ∈ 𝐶 ) ) → ( 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ) )
99 37 98 sylan2br ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ∧ 𝑓 ∈ 𝐶 ) ) → ( 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ) )
100 99 anassrs ⊢ ( ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) ∧ 𝑓 ∈ 𝐶 ) → ( 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ) )
101 100 rexlimdva ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ∧ ( 𝑑 ∈ 𝐴 ∧ 𝑒 ∈ 𝐵 ) ) → ( ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ) )
102 101 rexlimdvva ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ∃ 𝑑 ∈ 𝐴 ∃ 𝑒 ∈ 𝐵 ∃ 𝑓 ∈ 𝐶 𝑞 = ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ → ( 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ) )
103 36 102 syl5bi ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) → ( 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ) )
104 103 pm5.32d ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ) )
105 opex ⊢ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ V
106 vex ⊢ 𝑞 ∈ V
107 106 elpred ⊢ ( ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∈ V → ( 𝑞 ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ) )
108 105 107 ax-mp ⊢ ( 𝑞 ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 𝑈 ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) )
109 elin ⊢ ( 𝑞 ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ↔ ( 𝑞 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑞 ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) )
110 104 108 109 3bitr4g ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( 𝑞 ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ↔ 𝑞 ∈ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) ) )
111 110 eqrdv ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) = ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) )
112 predss ⊢ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝐴
113 112 a1i ⊢ ( 𝑎 ∈ 𝐴 → Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ 𝐴 )
114 snssi ⊢ ( 𝑎 ∈ 𝐴 → { 𝑎 } ⊆ 𝐴 )
115 113 114 unssd ⊢ ( 𝑎 ∈ 𝐴 → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ⊆ 𝐴 )
116 115 3ad2ant1 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ⊆ 𝐴 )
117 predss ⊢ Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ 𝐵
118 117 a1i ⊢ ( 𝑏 ∈ 𝐵 → Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ 𝐵 )
119 snssi ⊢ ( 𝑏 ∈ 𝐵 → { 𝑏 } ⊆ 𝐵 )
120 118 119 unssd ⊢ ( 𝑏 ∈ 𝐵 → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ⊆ 𝐵 )
121 120 3ad2ant2 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ⊆ 𝐵 )
122 xpss12 ⊢ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ⊆ 𝐴 ∧ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ⊆ 𝐵 ) → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ⊆ ( 𝐴 × 𝐵 ) )
123 116 121 122 syl2anc ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ⊆ ( 𝐴 × 𝐵 ) )
124 predss ⊢ Pred ( 𝑇 , 𝐶 , 𝑐 ) ⊆ 𝐶
125 124 a1i ⊢ ( 𝑐 ∈ 𝐶 → Pred ( 𝑇 , 𝐶 , 𝑐 ) ⊆ 𝐶 )
126 snssi ⊢ ( 𝑐 ∈ 𝐶 → { 𝑐 } ⊆ 𝐶 )
127 125 126 unssd ⊢ ( 𝑐 ∈ 𝐶 → ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ⊆ 𝐶 )
128 127 3ad2ant3 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ⊆ 𝐶 )
129 xpss12 ⊢ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) ⊆ ( 𝐴 × 𝐵 ) ∧ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ⊆ 𝐶 ) → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
130 123 128 129 syl2anc ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
131 130 ssdifssd ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
132 sseqin2 ⊢ ( ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ⊆ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ↔ ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) )
133 131 132 sylib ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∩ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) )
134 111 133 eqtrd ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) )
135 13 25 35 134 vtocl3ga ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ∪ { 𝑋 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑌 ) ∪ { 𝑌 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑍 ) ∪ { 𝑍 } ) ) ∖ { ⟨ ⟨ 𝑋 , 𝑌 ⟩ , 𝑍 ⟩ } ) )