Metamath Proof Explorer

Theorem xpord3inddlem

Description: Induction over the triple Cartesian product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 2-Feb-2025)

Ref Expression
Hypotheses xpord3.1 ⊢ 𝑈 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑦 ∈ ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑥 ) ) = ( 1st ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑆 ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑥 ) ) = ( 2nd ‘ ( 1st ‘ 𝑦 ) ) ) ∧ ( ( 2nd ‘ 𝑥 ) 𝑇 ( 2nd ‘ 𝑦 ) ∨ ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
xpord3inddlem.x ⊢ ( 𝜅 → 𝑋 ∈ 𝐴 )
xpord3inddlem.y ⊢ ( 𝜅 → 𝑌 ∈ 𝐵 )
xpord3inddlem.z ⊢ ( 𝜅 → 𝑍 ∈ 𝐶 )
xpord3inddlem.1 ⊢ ( 𝜅 → 𝑅 Fr 𝐴 )
xpord3inddlem.2 ⊢ ( 𝜅 → 𝑅 Po 𝐴 )
xpord3inddlem.3 ⊢ ( 𝜅 → 𝑅 Se 𝐴 )
xpord3inddlem.4 ⊢ ( 𝜅 → 𝑆 Fr 𝐵 )
xpord3inddlem.5 ⊢ ( 𝜅 → 𝑆 Po 𝐵 )
xpord3inddlem.6 ⊢ ( 𝜅 → 𝑆 Se 𝐵 )
xpord3inddlem.7 ⊢ ( 𝜅 → 𝑇 Fr 𝐶 )
xpord3inddlem.8 ⊢ ( 𝜅 → 𝑇 Po 𝐶 )
xpord3inddlem.9 ⊢ ( 𝜅 → 𝑇 Se 𝐶 )
xpord3inddlem.10 ⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜓 ) )
xpord3inddlem.11 ⊢ ( 𝑏 = 𝑒 → ( 𝜓 ↔ 𝜒 ) )
xpord3inddlem.12 ⊢ ( 𝑐 = 𝑓 → ( 𝜒 ↔ 𝜃 ) )
xpord3inddlem.13 ⊢ ( 𝑎 = 𝑑 → ( 𝜏 ↔ 𝜃 ) )
xpord3inddlem.14 ⊢ ( 𝑏 = 𝑒 → ( 𝜂 ↔ 𝜏 ) )
xpord3inddlem.15 ⊢ ( 𝑏 = 𝑒 → ( 𝜁 ↔ 𝜃 ) )
xpord3inddlem.16 ⊢ ( 𝑐 = 𝑓 → ( 𝜎 ↔ 𝜏 ) )
xpord3inddlem.17 ⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜌 ) )
xpord3inddlem.18 ⊢ ( 𝑏 = 𝑌 → ( 𝜌 ↔ 𝜇 ) )
xpord3inddlem.19 ⊢ ( 𝑐 = 𝑍 → ( 𝜇 ↔ 𝜆 ) )
xpord3inddlem.i ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) → 𝜑 ) )
Assertion xpord3inddlem ( 𝜅 → 𝜆 )

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 xpord3inddlem.x ⊢ ( 𝜅 → 𝑋 ∈ 𝐴 )
3 xpord3inddlem.y ⊢ ( 𝜅 → 𝑌 ∈ 𝐵 )
4 xpord3inddlem.z ⊢ ( 𝜅 → 𝑍 ∈ 𝐶 )
5 xpord3inddlem.1 ⊢ ( 𝜅 → 𝑅 Fr 𝐴 )
6 xpord3inddlem.2 ⊢ ( 𝜅 → 𝑅 Po 𝐴 )
7 xpord3inddlem.3 ⊢ ( 𝜅 → 𝑅 Se 𝐴 )
8 xpord3inddlem.4 ⊢ ( 𝜅 → 𝑆 Fr 𝐵 )
9 xpord3inddlem.5 ⊢ ( 𝜅 → 𝑆 Po 𝐵 )
10 xpord3inddlem.6 ⊢ ( 𝜅 → 𝑆 Se 𝐵 )
11 xpord3inddlem.7 ⊢ ( 𝜅 → 𝑇 Fr 𝐶 )
12 xpord3inddlem.8 ⊢ ( 𝜅 → 𝑇 Po 𝐶 )
13 xpord3inddlem.9 ⊢ ( 𝜅 → 𝑇 Se 𝐶 )
14 xpord3inddlem.10 ⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜓 ) )
15 xpord3inddlem.11 ⊢ ( 𝑏 = 𝑒 → ( 𝜓 ↔ 𝜒 ) )
16 xpord3inddlem.12 ⊢ ( 𝑐 = 𝑓 → ( 𝜒 ↔ 𝜃 ) )
17 xpord3inddlem.13 ⊢ ( 𝑎 = 𝑑 → ( 𝜏 ↔ 𝜃 ) )
18 xpord3inddlem.14 ⊢ ( 𝑏 = 𝑒 → ( 𝜂 ↔ 𝜏 ) )
19 xpord3inddlem.15 ⊢ ( 𝑏 = 𝑒 → ( 𝜁 ↔ 𝜃 ) )
20 xpord3inddlem.16 ⊢ ( 𝑐 = 𝑓 → ( 𝜎 ↔ 𝜏 ) )
21 xpord3inddlem.17 ⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜌 ) )
22 xpord3inddlem.18 ⊢ ( 𝑏 = 𝑌 → ( 𝜌 ↔ 𝜇 ) )
23 xpord3inddlem.19 ⊢ ( 𝑐 = 𝑍 → ( 𝜇 ↔ 𝜆 ) )
24 xpord3inddlem.i ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) → 𝜑 ) )
25 1 5 8 11 frxp3 ⊢ ( 𝜅 → 𝑈 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
26 1 6 9 12 poxp3 ⊢ ( 𝜅 → 𝑈 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
27 1 7 10 13 sexp3 ⊢ ( 𝜅 → 𝑈 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
28 bi2.04 ⊢ ( ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → ( 𝜅 → 𝜃 ) ) ↔ ( 𝜅 → ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
29 28 3albii ⊢ ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → ( 𝜅 → 𝜃 ) ) ↔ ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( 𝜅 → ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
30 19.21v ⊢ ( ∀ 𝑓 ( 𝜅 → ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) ↔ ( 𝜅 → ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
31 30 2albii ⊢ ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( 𝜅 → ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) ↔ ∀ 𝑑 ∀ 𝑒 ( 𝜅 → ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
32 19.21v ⊢ ( ∀ 𝑒 ( 𝜅 → ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) ↔ ( 𝜅 → ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
33 32 albii ⊢ ( ∀ 𝑑 ∀ 𝑒 ( 𝜅 → ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) ↔ ∀ 𝑑 ( 𝜅 → ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
34 19.21v ⊢ ( ∀ 𝑑 ( 𝜅 → ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) ↔ ( 𝜅 → ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
35 33 34 bitri ⊢ ( ∀ 𝑑 ∀ 𝑒 ( 𝜅 → ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) ↔ ( 𝜅 → ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
36 31 35 bitri ⊢ ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( 𝜅 → ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) ↔ ( 𝜅 → ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
37 29 36 bitri ⊢ ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → ( 𝜅 → 𝜃 ) ) ↔ ( 𝜅 → ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) )
38 1 xpord3pred ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) )
39 38 adantl ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) )
40 39 eleq2d ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ↔ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ) )
41 40 imbi1d ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ↔ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) → 𝜃 ) ) )
42 eldifsn ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ↔ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ≠ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) )
43 otelxp ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ↔ ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) )
44 vex ⊢ 𝑑 ∈ V
45 vex ⊢ 𝑒 ∈ V
46 vex ⊢ 𝑓 ∈ V
47 44 45 46 otthne ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ≠ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
48 43 47 anbi12i ⊢ ( ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ≠ ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) ↔ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
49 42 48 bitri ⊢ ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) ↔ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
50 49 imbi1i ⊢ ( ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ } ) → 𝜃 ) ↔ ( ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) → 𝜃 ) )
51 41 50 bitrdi ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ↔ ( ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) → 𝜃 ) ) )
52 impexp ⊢ ( ( ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) → 𝜃 ) ↔ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
53 51 52 bitrdi ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ↔ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) ) )
54 53 albidv ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ↔ ∀ 𝑓 ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) ) )
55 54 2albidv ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ↔ ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) ) )
56 r3al ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
57 56 bicomi ⊢ ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) ↔ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
58 55 57 bitrdi ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ↔ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
59 ssun1 ⊢ Pred ( 𝑇 , 𝐶 , 𝑐 ) ⊆ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } )
60 ssralv ⊢ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ⊆ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) → ( ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
61 59 60 ax-mp ⊢ ( ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
62 61 ralimi ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
63 ssun1 ⊢ Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } )
64 ssralv ⊢ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) → ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
65 63 64 ax-mp ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
66 62 65 syl ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
67 66 ralimi ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
68 ssun1 ⊢ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } )
69 ssralv ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
70 68 69 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
71 67 70 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
72 71 adantl ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
73 predpoirr ⊢ ( 𝑇 Po 𝐶 → ¬ 𝑐 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) )
74 12 73 syl ⊢ ( 𝜅 → ¬ 𝑐 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) )
75 eleq1 ⊢ ( 𝑓 = 𝑐 → ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ↔ 𝑐 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) )
76 75 notbid ⊢ ( 𝑓 = 𝑐 → ( ¬ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ↔ ¬ 𝑐 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) )
77 74 76 syl5ibrcom ⊢ ( 𝜅 → ( 𝑓 = 𝑐 → ¬ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) )
78 77 necon2ad ⊢ ( 𝜅 → ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → 𝑓 ≠ 𝑐 ) )
79 78 imp ⊢ ( ( 𝜅 ∧ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) → 𝑓 ≠ 𝑐 )
80 79 3mix3d ⊢ ( ( 𝜅 ∧ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) → ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
81 pm2.27 ⊢ ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → 𝜃 ) )
82 80 81 syl ⊢ ( ( 𝜅 ∧ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → 𝜃 ) )
83 82 ralimdva ⊢ ( 𝜅 → ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ) )
84 83 ralimdv ⊢ ( 𝜅 → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ) )
85 84 ralimdv ⊢ ( 𝜅 → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ) )
86 85 adantr ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ) )
87 72 86 mpd ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 )
88 ssun2 ⊢ { 𝑐 } ⊆ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } )
89 ssralv ⊢ ( { 𝑐 } ⊆ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) → ( ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
90 88 89 ax-mp ⊢ ( ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
91 90 ralimi ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
92 ssralv ⊢ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) → ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
93 63 92 ax-mp ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
94 91 93 syl ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
95 94 ralimi ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
96 ssralv ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
97 68 96 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
98 95 97 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
99 vex ⊢ 𝑐 ∈ V
100 biidd ⊢ ( 𝑓 = 𝑐 → ( 𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎 ) )
101 biidd ⊢ ( 𝑓 = 𝑐 → ( 𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏 ) )
102 neeq1 ⊢ ( 𝑓 = 𝑐 → ( 𝑓 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐 ) )
103 100 101 102 3orbi123d ⊢ ( 𝑓 = 𝑐 → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) )
104 16 equcoms ⊢ ( 𝑓 = 𝑐 → ( 𝜒 ↔ 𝜃 ) )
105 104 bicomd ⊢ ( 𝑓 = 𝑐 → ( 𝜃 ↔ 𝜒 ) )
106 103 105 imbi12d ⊢ ( 𝑓 = 𝑐 → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) ) )
107 99 106 ralsn ⊢ ( ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) )
108 107 2ralbii ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) )
109 98 108 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) )
110 109 adantl ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) )
111 predpoirr ⊢ ( 𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) )
112 9 111 syl ⊢ ( 𝜅 → ¬ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) )
113 eleq1 ⊢ ( 𝑒 = 𝑏 → ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) )
114 113 notbid ⊢ ( 𝑒 = 𝑏 → ( ¬ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ ¬ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) )
115 112 114 syl5ibrcom ⊢ ( 𝜅 → ( 𝑒 = 𝑏 → ¬ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) )
116 115 necon2ad ⊢ ( 𝜅 → ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → 𝑒 ≠ 𝑏 ) )
117 116 imp ⊢ ( ( 𝜅 ∧ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) → 𝑒 ≠ 𝑏 )
118 117 3mix2d ⊢ ( ( 𝜅 ∧ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) → ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) )
119 pm2.27 ⊢ ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) → 𝜒 ) )
120 118 119 syl ⊢ ( ( 𝜅 ∧ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) → 𝜒 ) )
121 120 ralimdva ⊢ ( 𝜅 → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ) )
122 121 ralimdv ⊢ ( 𝜅 → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ) )
123 122 adantr ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ) )
124 110 123 mpd ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 )
125 ssun2 ⊢ { 𝑏 } ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } )
126 ssralv ⊢ ( { 𝑏 } ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) → ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
127 125 126 ax-mp ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
128 62 127 syl ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
129 128 ralimi ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
130 ssralv ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
131 68 130 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
132 129 131 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
133 vex ⊢ 𝑏 ∈ V
134 biidd ⊢ ( 𝑒 = 𝑏 → ( 𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎 ) )
135 neeq1 ⊢ ( 𝑒 = 𝑏 → ( 𝑒 ≠ 𝑏 ↔ 𝑏 ≠ 𝑏 ) )
136 biidd ⊢ ( 𝑒 = 𝑏 → ( 𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐 ) )
137 134 135 136 3orbi123d ⊢ ( 𝑒 = 𝑏 → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
138 19 equcoms ⊢ ( 𝑒 = 𝑏 → ( 𝜁 ↔ 𝜃 ) )
139 138 bicomd ⊢ ( 𝑒 = 𝑏 → ( 𝜃 ↔ 𝜁 ) )
140 137 139 imbi12d ⊢ ( 𝑒 = 𝑏 → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) ) )
141 140 ralbidv ⊢ ( 𝑒 = 𝑏 → ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) ) )
142 133 141 ralsn ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) )
143 142 ralbii ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) )
144 132 143 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) )
145 144 adantl ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) )
146 79 3mix3d ⊢ ( ( 𝜅 ∧ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) → ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
147 pm2.27 ⊢ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) → 𝜁 ) )
148 146 147 syl ⊢ ( ( 𝜅 ∧ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) → 𝜁 ) )
149 148 ralimdva ⊢ ( 𝜅 → ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) )
150 149 ralimdv ⊢ ( 𝜅 → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) )
151 150 adantr ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) )
152 145 151 mpd ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 )
153 87 124 152 3jca ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) )
154 ssralv ⊢ ( { 𝑏 } ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) → ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
155 125 154 ax-mp ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
156 91 155 syl ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
157 156 ralimi ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
158 ssralv ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
159 68 158 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
160 157 159 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
161 107 ralbii ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ { 𝑏 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) )
162 biidd ⊢ ( 𝑒 = 𝑏 → ( 𝑐 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐 ) )
163 134 135 162 3orbi123d ⊢ ( 𝑒 = 𝑏 → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) )
164 15 equcoms ⊢ ( 𝑒 = 𝑏 → ( 𝜓 ↔ 𝜒 ) )
165 164 bicomd ⊢ ( 𝑒 = 𝑏 → ( 𝜒 ↔ 𝜓 ) )
166 163 165 imbi12d ⊢ ( 𝑒 = 𝑏 → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) ) )
167 133 166 ralsn ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) )
168 161 167 bitri ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) )
169 168 ralbii ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) )
170 160 169 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) )
171 170 adantl ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) )
172 predpoirr ⊢ ( 𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) )
173 6 172 syl ⊢ ( 𝜅 → ¬ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) )
174 eleq1 ⊢ ( 𝑑 = 𝑎 → ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
175 174 notbid ⊢ ( 𝑑 = 𝑎 → ( ¬ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ ¬ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
176 173 175 syl5ibrcom ⊢ ( 𝜅 → ( 𝑑 = 𝑎 → ¬ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
177 176 necon2ad ⊢ ( 𝜅 → ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) → 𝑑 ≠ 𝑎 ) )
178 177 imp ⊢ ( ( 𝜅 ∧ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) → 𝑑 ≠ 𝑎 )
179 178 3mix1d ⊢ ( ( 𝜅 ∧ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) → ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) )
180 pm2.27 ⊢ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) → 𝜓 ) )
181 179 180 syl ⊢ ( ( 𝜅 ∧ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) → 𝜓 ) )
182 181 ralimdva ⊢ ( 𝜅 → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ) )
183 182 adantr ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ) )
184 171 183 mpd ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 )
185 ssun2 ⊢ { 𝑎 } ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } )
186 ssralv ⊢ ( { 𝑎 } ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
187 185 186 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
188 67 187 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
189 vex ⊢ 𝑎 ∈ V
190 neeq1 ⊢ ( 𝑑 = 𝑎 → ( 𝑑 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
191 biidd ⊢ ( 𝑑 = 𝑎 → ( 𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏 ) )
192 biidd ⊢ ( 𝑑 = 𝑎 → ( 𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐 ) )
193 190 191 192 3orbi123d ⊢ ( 𝑑 = 𝑎 → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
194 17 equcoms ⊢ ( 𝑑 = 𝑎 → ( 𝜏 ↔ 𝜃 ) )
195 194 bicomd ⊢ ( 𝑑 = 𝑎 → ( 𝜃 ↔ 𝜏 ) )
196 193 195 imbi12d ⊢ ( 𝑑 = 𝑎 → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ) )
197 196 2ralbidv ⊢ ( 𝑑 = 𝑎 → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ) )
198 189 197 ralsn ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) )
199 188 198 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) )
200 199 adantl ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) )
201 79 3mix3d ⊢ ( ( 𝜅 ∧ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) → ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
202 pm2.27 ⊢ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) → 𝜏 ) )
203 201 202 syl ⊢ ( ( 𝜅 ∧ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) → 𝜏 ) )
204 203 ralimdva ⊢ ( 𝜅 → ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ) )
205 204 ralimdv ⊢ ( 𝜅 → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ) )
206 205 adantr ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ) )
207 200 206 mpd ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 )
208 ssralv ⊢ ( { 𝑎 } ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
209 185 208 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
210 95 209 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
211 196 2ralbidv ⊢ ( 𝑑 = 𝑎 → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ) )
212 189 211 ralsn ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) )
213 biidd ⊢ ( 𝑓 = 𝑐 → ( 𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
214 213 101 102 3orbi123d ⊢ ( 𝑓 = 𝑐 → ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) )
215 20 bicomd ⊢ ( 𝑐 = 𝑓 → ( 𝜏 ↔ 𝜎 ) )
216 215 equcoms ⊢ ( 𝑓 = 𝑐 → ( 𝜏 ↔ 𝜎 ) )
217 214 216 imbi12d ⊢ ( 𝑓 = 𝑐 → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) ) )
218 99 217 ralsn ⊢ ( ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) )
219 218 ralbii ⊢ ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) )
220 212 219 bitri ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) )
221 210 220 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) )
222 221 adantl ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) )
223 117 3mix2d ⊢ ( ( 𝜅 ∧ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) → ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) )
224 pm2.27 ⊢ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) → 𝜎 ) )
225 223 224 syl ⊢ ( ( 𝜅 ∧ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) → 𝜎 ) )
226 225 ralimdva ⊢ ( 𝜅 → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) )
227 226 adantr ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) )
228 222 227 mpd ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 )
229 184 207 228 3jca ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) )
230 ssralv ⊢ ( { 𝑎 } ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
231 185 230 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
232 129 231 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
233 196 2ralbidv ⊢ ( 𝑑 = 𝑎 → ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ) )
234 189 233 ralsn ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) )
235 biidd ⊢ ( 𝑒 = 𝑏 → ( 𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
236 235 135 136 3orbi123d ⊢ ( 𝑒 = 𝑏 → ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
237 equcomi ⊢ ( 𝑒 = 𝑏 → 𝑏 = 𝑒 )
238 bicom1 ⊢ ( ( 𝜂 ↔ 𝜏 ) → ( 𝜏 ↔ 𝜂 ) )
239 237 18 238 3syl ⊢ ( 𝑒 = 𝑏 → ( 𝜏 ↔ 𝜂 ) )
240 236 239 imbi12d ⊢ ( 𝑒 = 𝑏 → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) ) )
241 240 ralbidv ⊢ ( 𝑒 = 𝑏 → ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) ) )
242 133 241 ralsn ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) )
243 234 242 bitri ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) )
244 232 243 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) )
245 244 adantl ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) )
246 79 3mix3d ⊢ ( ( 𝜅 ∧ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) → ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
247 pm2.27 ⊢ ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) → 𝜂 ) )
248 246 247 syl ⊢ ( ( 𝜅 ∧ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) → 𝜂 ) )
249 248 ralimdva ⊢ ( 𝜅 → ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) )
250 249 adantr ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) )
251 245 250 mpd ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 )
252 153 229 251 3jca ⊢ ( ( 𝜅 ∧ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) → ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) )
253 252 ex ⊢ ( 𝜅 → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) ) )
254 253 adantr ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) ) )
255 254 24 syld ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → 𝜑 ) )
256 58 255 sylbid ⊢ ( ( 𝜅 ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) ) → ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) → 𝜑 ) )
257 256 expcom ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( 𝜅 → ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) → 𝜑 ) ) )
258 257 a2d ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( 𝜅 → ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → 𝜃 ) ) → ( 𝜅 → 𝜑 ) ) )
259 37 258 biimtrid ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ 𝑑 , 𝑒 , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ 𝑎 , 𝑏 , 𝑐 ⟩ ) → ( 𝜅 → 𝜃 ) ) → ( 𝜅 → 𝜑 ) ) )
260 14 imbi2d ⊢ ( 𝑎 = 𝑑 → ( ( 𝜅 → 𝜑 ) ↔ ( 𝜅 → 𝜓 ) ) )
261 15 imbi2d ⊢ ( 𝑏 = 𝑒 → ( ( 𝜅 → 𝜓 ) ↔ ( 𝜅 → 𝜒 ) ) )
262 16 imbi2d ⊢ ( 𝑐 = 𝑓 → ( ( 𝜅 → 𝜒 ) ↔ ( 𝜅 → 𝜃 ) ) )
263 21 imbi2d ⊢ ( 𝑎 = 𝑋 → ( ( 𝜅 → 𝜑 ) ↔ ( 𝜅 → 𝜌 ) ) )
264 22 imbi2d ⊢ ( 𝑏 = 𝑌 → ( ( 𝜅 → 𝜌 ) ↔ ( 𝜅 → 𝜇 ) ) )
265 23 imbi2d ⊢ ( 𝑐 = 𝑍 → ( ( 𝜅 → 𝜇 ) ↔ ( 𝜅 → 𝜆 ) ) )
266 259 260 261 262 263 264 265 frpoins3xp3g ⊢ ( ( ( 𝑈 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑈 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑈 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → ( 𝜅 → 𝜆 ) )
267 25 26 27 2 3 4 266 syl33anc ⊢ ( 𝜅 → ( 𝜅 → 𝜆 ) )
268 267 pm2.43i ⊢ ( 𝜅 → 𝜆 )