Metamath Proof Explorer

Theorem xpord3ind

Description: Induction over the triple cross product ordering. Note that the substitutions cover all possible cases of membership in the predecessor class. (Contributed by Scott Fenton, 4-Sep-2024)

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 ‘ 𝑦 ) ) ) ∧ 𝑥 ≠ 𝑦 ) ) }
xpord3ind.1 ⊢ 𝑅 Fr 𝐴
xpord3ind.2 ⊢ 𝑅 Po 𝐴
xpord3ind.3 ⊢ 𝑅 Se 𝐴
xpord3ind.4 ⊢ 𝑆 Fr 𝐵
xpord3ind.5 ⊢ 𝑆 Po 𝐵
xpord3ind.6 ⊢ 𝑆 Se 𝐵
xpord3ind.7 ⊢ 𝑇 Fr 𝐶
xpord3ind.8 ⊢ 𝑇 Po 𝐶
xpord3ind.9 ⊢ 𝑇 Se 𝐶
xpord3ind.10 ⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜓 ) )
xpord3ind.11 ⊢ ( 𝑏 = 𝑒 → ( 𝜓 ↔ 𝜒 ) )
xpord3ind.12 ⊢ ( 𝑐 = 𝑓 → ( 𝜒 ↔ 𝜃 ) )
xpord3ind.13 ⊢ ( 𝑎 = 𝑑 → ( 𝜏 ↔ 𝜃 ) )
xpord3ind.14 ⊢ ( 𝑏 = 𝑒 → ( 𝜂 ↔ 𝜏 ) )
xpord3ind.15 ⊢ ( 𝑏 = 𝑒 → ( 𝜁 ↔ 𝜃 ) )
xpord3ind.16 ⊢ ( 𝑐 = 𝑓 → ( 𝜎 ↔ 𝜏 ) )
xpord3ind.17 ⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜌 ) )
xpord3ind.18 ⊢ ( 𝑏 = 𝑌 → ( 𝜌 ↔ 𝜇 ) )
xpord3ind.19 ⊢ ( 𝑐 = 𝑍 → ( 𝜇 ↔ 𝜆 ) )
xpord3ind.i ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) → 𝜑 ) )
Assertion xpord3ind ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝜆 )

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 xpord3ind.1 ⊢ 𝑅 Fr 𝐴
3 xpord3ind.2 ⊢ 𝑅 Po 𝐴
4 xpord3ind.3 ⊢ 𝑅 Se 𝐴
5 xpord3ind.4 ⊢ 𝑆 Fr 𝐵
6 xpord3ind.5 ⊢ 𝑆 Po 𝐵
7 xpord3ind.6 ⊢ 𝑆 Se 𝐵
8 xpord3ind.7 ⊢ 𝑇 Fr 𝐶
9 xpord3ind.8 ⊢ 𝑇 Po 𝐶
10 xpord3ind.9 ⊢ 𝑇 Se 𝐶
11 xpord3ind.10 ⊢ ( 𝑎 = 𝑑 → ( 𝜑 ↔ 𝜓 ) )
12 xpord3ind.11 ⊢ ( 𝑏 = 𝑒 → ( 𝜓 ↔ 𝜒 ) )
13 xpord3ind.12 ⊢ ( 𝑐 = 𝑓 → ( 𝜒 ↔ 𝜃 ) )
14 xpord3ind.13 ⊢ ( 𝑎 = 𝑑 → ( 𝜏 ↔ 𝜃 ) )
15 xpord3ind.14 ⊢ ( 𝑏 = 𝑒 → ( 𝜂 ↔ 𝜏 ) )
16 xpord3ind.15 ⊢ ( 𝑏 = 𝑒 → ( 𝜁 ↔ 𝜃 ) )
17 xpord3ind.16 ⊢ ( 𝑐 = 𝑓 → ( 𝜎 ↔ 𝜏 ) )
18 xpord3ind.17 ⊢ ( 𝑎 = 𝑋 → ( 𝜑 ↔ 𝜌 ) )
19 xpord3ind.18 ⊢ ( 𝑏 = 𝑌 → ( 𝜌 ↔ 𝜇 ) )
20 xpord3ind.19 ⊢ ( 𝑐 = 𝑍 → ( 𝜇 ↔ 𝜆 ) )
21 xpord3ind.i ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) → 𝜑 ) )
22 2 a1i ⊢ ( ⊤ → 𝑅 Fr 𝐴 )
23 5 a1i ⊢ ( ⊤ → 𝑆 Fr 𝐵 )
24 8 a1i ⊢ ( ⊤ → 𝑇 Fr 𝐶 )
25 1 22 23 24 frxp3 ⊢ ( ⊤ → 𝑈 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
26 25 mptru ⊢ 𝑈 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 )
27 3 a1i ⊢ ( ⊤ → 𝑅 Po 𝐴 )
28 6 a1i ⊢ ( ⊤ → 𝑆 Po 𝐵 )
29 9 a1i ⊢ ( ⊤ → 𝑇 Po 𝐶 )
30 1 27 28 29 poxp3 ⊢ ( ⊤ → 𝑈 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
31 30 mptru ⊢ 𝑈 Po ( ( 𝐴 × 𝐵 ) × 𝐶 )
32 4 a1i ⊢ ( ⊤ → 𝑅 Se 𝐴 )
33 7 a1i ⊢ ( ⊤ → 𝑆 Se 𝐵 )
34 10 a1i ⊢ ( ⊤ → 𝑇 Se 𝐶 )
35 1 32 33 34 sexp3 ⊢ ( ⊤ → 𝑈 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
36 35 mptru ⊢ 𝑈 Se ( ( 𝐴 × 𝐵 ) × 𝐶 )
37 26 31 36 3pm3.2i ⊢ ( 𝑈 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑈 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑈 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) )
38 1 xpord3pred ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) = ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) )
39 38 eleq2d ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ↔ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ) )
40 39 imbi1d ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) → 𝜃 ) ↔ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) → 𝜃 ) ) )
41 eldifsn ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ↔ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ≠ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) )
42 ot2elxp ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ↔ ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) )
43 vex ⊢ 𝑑 ∈ V
44 vex ⊢ 𝑒 ∈ V
45 vex ⊢ 𝑓 ∈ V
46 43 44 45 otthne ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ≠ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
47 42 46 anbi12i ⊢ ( ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ≠ ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) ↔ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
48 41 47 bitri ⊢ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) ↔ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
49 48 imbi1i ⊢ ( ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) → 𝜃 ) ↔ ( ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) → 𝜃 ) )
50 impexp ⊢ ( ( ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∧ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) → 𝜃 ) ↔ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
51 49 50 bitr2i ⊢ ( ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) ↔ ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ ( ( ( ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) × ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ) × ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) ∖ { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ } ) → 𝜃 ) )
52 40 51 bitr4di ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) → 𝜃 ) ↔ ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) ) )
53 52 albidv ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ∀ 𝑓 ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) → 𝜃 ) ↔ ∀ 𝑓 ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) ) )
54 53 2albidv ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) → 𝜃 ) ↔ ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) ) )
55 r3al ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ( 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∧ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∧ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ) → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
56 54 55 bitr4di ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) → 𝜃 ) ↔ ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
57 ssun1 ⊢ Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } )
58 ssralv ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
59 57 58 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
60 ssun1 ⊢ Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } )
61 ssralv ⊢ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) → ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
62 60 61 ax-mp ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
63 ssun1 ⊢ Pred ( 𝑇 , 𝐶 , 𝑐 ) ⊆ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } )
64 ssralv ⊢ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ⊆ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) → ( ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
65 63 64 ax-mp ⊢ ( ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
66 65 ralimi ⊢ ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
67 62 66 syl ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
68 67 ralimi ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
69 predpoirr ⊢ ( 𝑇 Po 𝐶 → ¬ 𝑐 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) )
70 9 69 ax-mp ⊢ ¬ 𝑐 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 )
71 eleq1w ⊢ ( 𝑓 = 𝑐 → ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ↔ 𝑐 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ) )
72 70 71 mtbiri ⊢ ( 𝑓 = 𝑐 → ¬ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) )
73 72 necon2ai ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → 𝑓 ≠ 𝑐 )
74 73 3mix3d ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
75 pm2.27 ⊢ ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → 𝜃 ) )
76 74 75 syl ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → 𝜃 ) )
77 76 ralimia ⊢ ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 )
78 77 2ralimi ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 )
79 59 68 78 3syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 )
80 ssun2 ⊢ { 𝑐 } ⊆ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } )
81 ssralv ⊢ ( { 𝑐 } ⊆ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) → ( ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
82 80 81 ax-mp ⊢ ( ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
83 82 ralimi ⊢ ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
84 62 83 syl ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
85 84 ralimi ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
86 59 85 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
87 vex ⊢ 𝑐 ∈ V
88 biidd ⊢ ( 𝑓 = 𝑐 → ( 𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎 ) )
89 biidd ⊢ ( 𝑓 = 𝑐 → ( 𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏 ) )
90 neeq1 ⊢ ( 𝑓 = 𝑐 → ( 𝑓 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐 ) )
91 88 89 90 3orbi123d ⊢ ( 𝑓 = 𝑐 → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) )
92 13 bicomd ⊢ ( 𝑐 = 𝑓 → ( 𝜃 ↔ 𝜒 ) )
93 92 equcoms ⊢ ( 𝑓 = 𝑐 → ( 𝜃 ↔ 𝜒 ) )
94 91 93 imbi12d ⊢ ( 𝑓 = 𝑐 → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) ) )
95 87 94 ralsn ⊢ ( ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) )
96 95 2ralbii ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) )
97 86 96 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) )
98 predpoirr ⊢ ( 𝑆 Po 𝐵 → ¬ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) )
99 6 98 ax-mp ⊢ ¬ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 )
100 eleq1w ⊢ ( 𝑒 = 𝑏 → ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ↔ 𝑏 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ) )
101 99 100 mtbiri ⊢ ( 𝑒 = 𝑏 → ¬ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) )
102 101 necon2ai ⊢ ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → 𝑒 ≠ 𝑏 )
103 102 3mix2d ⊢ ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) )
104 pm2.27 ⊢ ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) → 𝜒 ) )
105 103 104 syl ⊢ ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) → 𝜒 ) )
106 105 ralimia ⊢ ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 )
107 106 ralimi ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 )
108 97 107 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 )
109 ssun2 ⊢ { 𝑏 } ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } )
110 ssralv ⊢ ( { 𝑏 } ⊆ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) → ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
111 109 110 ax-mp ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
112 65 ralimi ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
113 111 112 syl ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
114 113 ralimi ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
115 59 114 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
116 vex ⊢ 𝑏 ∈ V
117 biidd ⊢ ( 𝑒 = 𝑏 → ( 𝑑 ≠ 𝑎 ↔ 𝑑 ≠ 𝑎 ) )
118 neeq1 ⊢ ( 𝑒 = 𝑏 → ( 𝑒 ≠ 𝑏 ↔ 𝑏 ≠ 𝑏 ) )
119 biidd ⊢ ( 𝑒 = 𝑏 → ( 𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐 ) )
120 117 118 119 3orbi123d ⊢ ( 𝑒 = 𝑏 → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
121 equcom ⊢ ( 𝑏 = 𝑒 ↔ 𝑒 = 𝑏 )
122 bicom ⊢ ( ( 𝜁 ↔ 𝜃 ) ↔ ( 𝜃 ↔ 𝜁 ) )
123 16 121 122 3imtr3i ⊢ ( 𝑒 = 𝑏 → ( 𝜃 ↔ 𝜁 ) )
124 120 123 imbi12d ⊢ ( 𝑒 = 𝑏 → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) ) )
125 124 ralbidv ⊢ ( 𝑒 = 𝑏 → ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) ) )
126 116 125 ralsn ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) )
127 126 ralbii ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) )
128 115 127 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) )
129 73 3mix3d ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
130 pm2.27 ⊢ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) → 𝜁 ) )
131 129 130 syl ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) → 𝜁 ) )
132 131 ralimia ⊢ ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 )
133 132 ralimi ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜁 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 )
134 128 133 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 )
135 79 108 134 3jca ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) )
136 82 ralimi ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
137 111 136 syl ⊢ ( ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
138 137 ralimi ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
139 59 138 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
140 95 ralbii ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ { 𝑏 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) )
141 biidd ⊢ ( 𝑒 = 𝑏 → ( 𝑐 ≠ 𝑐 ↔ 𝑐 ≠ 𝑐 ) )
142 117 118 141 3orbi123d ⊢ ( 𝑒 = 𝑏 → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ↔ ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) )
143 12 bicomd ⊢ ( 𝑏 = 𝑒 → ( 𝜒 ↔ 𝜓 ) )
144 143 equcoms ⊢ ( 𝑒 = 𝑏 → ( 𝜒 ↔ 𝜓 ) )
145 142 144 imbi12d ⊢ ( 𝑒 = 𝑏 → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) ) )
146 116 145 ralsn ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜒 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) )
147 140 146 bitri ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) )
148 147 ralbii ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) )
149 139 148 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) )
150 predpoirr ⊢ ( 𝑅 Po 𝐴 → ¬ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) )
151 3 150 ax-mp ⊢ ¬ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 )
152 eleq1w ⊢ ( 𝑑 = 𝑎 → ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ↔ 𝑎 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ) )
153 151 152 mtbiri ⊢ ( 𝑑 = 𝑎 → ¬ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) )
154 153 necon2ai ⊢ ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) → 𝑑 ≠ 𝑎 )
155 154 3mix1d ⊢ ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) → ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) )
156 pm2.27 ⊢ ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) → 𝜓 ) )
157 155 156 syl ⊢ ( 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) → 𝜓 ) )
158 157 ralimia ⊢ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜓 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 )
159 149 158 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 )
160 ssun2 ⊢ { 𝑎 } ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } )
161 ssralv ⊢ ( { 𝑎 } ⊆ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ) )
162 160 161 ax-mp ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
163 67 ralimi ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
164 162 163 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
165 vex ⊢ 𝑎 ∈ V
166 neeq1 ⊢ ( 𝑑 = 𝑎 → ( 𝑑 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
167 biidd ⊢ ( 𝑑 = 𝑎 → ( 𝑒 ≠ 𝑏 ↔ 𝑒 ≠ 𝑏 ) )
168 biidd ⊢ ( 𝑑 = 𝑎 → ( 𝑓 ≠ 𝑐 ↔ 𝑓 ≠ 𝑐 ) )
169 166 167 168 3orbi123d ⊢ ( 𝑑 = 𝑎 → ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
170 14 equcoms ⊢ ( 𝑑 = 𝑎 → ( 𝜏 ↔ 𝜃 ) )
171 170 bicomd ⊢ ( 𝑑 = 𝑎 → ( 𝜃 ↔ 𝜏 ) )
172 169 171 imbi12d ⊢ ( 𝑑 = 𝑎 → ( ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ) )
173 172 2ralbidv ⊢ ( 𝑑 = 𝑎 → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ) )
174 165 173 ralsn ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) )
175 164 174 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) )
176 73 3mix3d ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
177 pm2.27 ⊢ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) → 𝜏 ) )
178 176 177 syl ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) → 𝜏 ) )
179 178 ralimia ⊢ ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 )
180 179 ralimi ⊢ ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 )
181 175 180 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 )
182 84 ralimi ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
183 162 182 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
184 172 2ralbidv ⊢ ( 𝑑 = 𝑎 → ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ) )
185 165 184 ralsn ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) )
186 biidd ⊢ ( 𝑓 = 𝑐 → ( 𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
187 186 89 90 3orbi123d ⊢ ( 𝑓 = 𝑐 → ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) ) )
188 17 bicomd ⊢ ( 𝑐 = 𝑓 → ( 𝜏 ↔ 𝜎 ) )
189 188 equcoms ⊢ ( 𝑓 = 𝑐 → ( 𝜏 ↔ 𝜎 ) )
190 187 189 imbi12d ⊢ ( 𝑓 = 𝑐 → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) ) )
191 87 190 ralsn ⊢ ( ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) )
192 191 ralbii ⊢ ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) )
193 185 192 bitri ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ { 𝑐 } ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) )
194 183 193 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) )
195 102 3mix2d ⊢ ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) )
196 pm2.27 ⊢ ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) → 𝜎 ) )
197 195 196 syl ⊢ ( 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) → 𝜎 ) )
198 197 ralimia ⊢ ( ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑐 ≠ 𝑐 ) → 𝜎 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 )
199 194 198 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 )
200 159 181 199 3jca ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) )
201 113 ralimi ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
202 162 201 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) )
203 172 2ralbidv ⊢ ( 𝑑 = 𝑎 → ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ) )
204 165 203 ralsn ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) )
205 biidd ⊢ ( 𝑒 = 𝑏 → ( 𝑎 ≠ 𝑎 ↔ 𝑎 ≠ 𝑎 ) )
206 205 118 119 3orbi123d ⊢ ( 𝑒 = 𝑏 → ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ↔ ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) ) )
207 15 equcoms ⊢ ( 𝑒 = 𝑏 → ( 𝜂 ↔ 𝜏 ) )
208 207 bicomd ⊢ ( 𝑒 = 𝑏 → ( 𝜏 ↔ 𝜂 ) )
209 206 208 imbi12d ⊢ ( 𝑒 = 𝑏 → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) ) )
210 209 ralbidv ⊢ ( 𝑒 = 𝑏 → ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) ) )
211 116 210 ralsn ⊢ ( ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜏 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) )
212 204 211 bitri ⊢ ( ∀ 𝑑 ∈ { 𝑎 } ∀ 𝑒 ∈ { 𝑏 } ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) ↔ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) )
213 202 212 sylib ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) )
214 73 3mix3d ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) )
215 pm2.27 ⊢ ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) → 𝜂 ) )
216 214 215 syl ⊢ ( 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) → ( ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) → 𝜂 ) )
217 216 ralimia ⊢ ( ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) ( ( 𝑎 ≠ 𝑎 ∨ 𝑏 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜂 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 )
218 213 217 syl ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 )
219 135 200 218 3jca ⊢ ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → ( ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜃 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜒 ∧ ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜁 ) ∧ ( ∀ 𝑑 ∈ Pred ( 𝑅 , 𝐴 , 𝑎 ) 𝜓 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜏 ∧ ∀ 𝑒 ∈ Pred ( 𝑆 , 𝐵 , 𝑏 ) 𝜎 ) ∧ ∀ 𝑓 ∈ Pred ( 𝑇 , 𝐶 , 𝑐 ) 𝜂 ) )
220 219 21 syl5 ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ∀ 𝑑 ∈ ( Pred ( 𝑅 , 𝐴 , 𝑎 ) ∪ { 𝑎 } ) ∀ 𝑒 ∈ ( Pred ( 𝑆 , 𝐵 , 𝑏 ) ∪ { 𝑏 } ) ∀ 𝑓 ∈ ( Pred ( 𝑇 , 𝐶 , 𝑐 ) ∪ { 𝑐 } ) ( ( 𝑑 ≠ 𝑎 ∨ 𝑒 ≠ 𝑏 ∨ 𝑓 ≠ 𝑐 ) → 𝜃 ) → 𝜑 ) )
221 56 220 sylbid ⊢ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ∧ 𝑐 ∈ 𝐶 ) → ( ∀ 𝑑 ∀ 𝑒 ∀ 𝑓 ( ⟨ ⟨ 𝑑 , 𝑒 ⟩ , 𝑓 ⟩ ∈ Pred ( 𝑈 , ( ( 𝐴 × 𝐵 ) × 𝐶 ) , ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ) → 𝜃 ) → 𝜑 ) )
222 221 11 12 13 18 19 20 frpoins3xp3g ⊢ ( ( ( 𝑈 Fr ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑈 Po ( ( 𝐴 × 𝐵 ) × 𝐶 ) ∧ 𝑈 Se ( ( 𝐴 × 𝐵 ) × 𝐶 ) ) ∧ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) ) → 𝜆 )
223 37 222 mpan ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐶 ) → 𝜆 )