Metamath Proof Explorer

Theorem no3indslem

Description: Triple induction over surreal numbers. Lemma with explicit relationship. (Contributed by Scott Fenton, 21-Aug-2024)

Ref Expression
Hypotheses no3indslem.a ⊢ 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) }
no3indslem.b ⊢ 𝑆 = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( 𝑐 ∈ ( ( No × No ) × No ) ∧ 𝑑 ∈ ( ( No × No ) × No ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑐 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑑 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑐 ) ) = ( 1st ‘ ( 1st ‘ 𝑑 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑐 ) ) 𝑅 ( 2nd ‘ ( 1st ‘ 𝑑 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑐 ) ) = ( 2nd ‘ ( 1st ‘ 𝑑 ) ) ) ∧ ( ( 2nd ‘ 𝑐 ) 𝑅 ( 2nd ‘ 𝑑 ) ∨ ( 2nd ‘ 𝑐 ) = ( 2nd ‘ 𝑑 ) ) ) ∧ 𝑐 ≠ 𝑑 ) ) }
no3indslem.1 ⊢ ( 𝑝 = 𝑞 → ( 𝜑 ↔ 𝜓 ) )
no3indslem.2 ⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜒 ) )
no3indslem.3 ⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( 𝜓 ↔ 𝜃 ) )
no3indslem.4 ⊢ ( 𝑢 = 𝑧 → ( 𝜃 ↔ 𝜏 ) )
no3indslem.5 ⊢ ( 𝑡 = 𝑦 → ( 𝜃 ↔ 𝜂 ) )
no3indslem.6 ⊢ ( 𝑢 = 𝑧 → ( 𝜂 ↔ 𝜁 ) )
no3indslem.7 ⊢ ( 𝑤 = 𝑥 → ( 𝜃 ↔ 𝜎 ) )
no3indslem.8 ⊢ ( 𝑢 = 𝑧 → ( 𝜎 ↔ 𝜌 ) )
no3indslem.9 ⊢ ( 𝑡 = 𝑦 → ( 𝜎 ↔ 𝜇 ) )
no3indslem.10 ⊢ ( 𝑥 = 𝐴 → ( 𝜒 ↔ 𝜆 ) )
no3indslem.11 ⊢ ( 𝑦 = 𝐵 → ( 𝜆 ↔ 𝜅 ) )
no3indslem.12 ⊢ ( 𝑧 = 𝐶 → ( 𝜅 ↔ 𝛻 ) )
no3indslem.i ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ( ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 ) ∧ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜁 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜌 ) ∧ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜇 ) → 𝜒 ) )
Assertion no3indslem ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝛻 )

Proof

Step Hyp Ref Expression
1 no3indslem.a ⊢ 𝑅 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ 𝑎 ∈ ( ( L ‘ 𝑏 ) ∪ ( R ‘ 𝑏 ) ) }
2 no3indslem.b ⊢ 𝑆 = { ⟨ 𝑐 , 𝑑 ⟩ ∣ ( 𝑐 ∈ ( ( No × No ) × No ) ∧ 𝑑 ∈ ( ( No × No ) × No ) ∧ ( ( ( ( 1st ‘ ( 1st ‘ 𝑐 ) ) 𝑅 ( 1st ‘ ( 1st ‘ 𝑑 ) ) ∨ ( 1st ‘ ( 1st ‘ 𝑐 ) ) = ( 1st ‘ ( 1st ‘ 𝑑 ) ) ) ∧ ( ( 2nd ‘ ( 1st ‘ 𝑐 ) ) 𝑅 ( 2nd ‘ ( 1st ‘ 𝑑 ) ) ∨ ( 2nd ‘ ( 1st ‘ 𝑐 ) ) = ( 2nd ‘ ( 1st ‘ 𝑑 ) ) ) ∧ ( ( 2nd ‘ 𝑐 ) 𝑅 ( 2nd ‘ 𝑑 ) ∨ ( 2nd ‘ 𝑐 ) = ( 2nd ‘ 𝑑 ) ) ) ∧ 𝑐 ≠ 𝑑 ) ) }
3 no3indslem.1 ⊢ ( 𝑝 = 𝑞 → ( 𝜑 ↔ 𝜓 ) )
4 no3indslem.2 ⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( 𝜑 ↔ 𝜒 ) )
5 no3indslem.3 ⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( 𝜓 ↔ 𝜃 ) )
6 no3indslem.4 ⊢ ( 𝑢 = 𝑧 → ( 𝜃 ↔ 𝜏 ) )
7 no3indslem.5 ⊢ ( 𝑡 = 𝑦 → ( 𝜃 ↔ 𝜂 ) )
8 no3indslem.6 ⊢ ( 𝑢 = 𝑧 → ( 𝜂 ↔ 𝜁 ) )
9 no3indslem.7 ⊢ ( 𝑤 = 𝑥 → ( 𝜃 ↔ 𝜎 ) )
10 no3indslem.8 ⊢ ( 𝑢 = 𝑧 → ( 𝜎 ↔ 𝜌 ) )
11 no3indslem.9 ⊢ ( 𝑡 = 𝑦 → ( 𝜎 ↔ 𝜇 ) )
12 no3indslem.10 ⊢ ( 𝑥 = 𝐴 → ( 𝜒 ↔ 𝜆 ) )
13 no3indslem.11 ⊢ ( 𝑦 = 𝐵 → ( 𝜆 ↔ 𝜅 ) )
14 no3indslem.12 ⊢ ( 𝑧 = 𝐶 → ( 𝜅 ↔ 𝛻 ) )
15 no3indslem.i ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ( ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 ) ∧ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜁 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜌 ) ∧ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜇 ) → 𝜒 ) )
16 1 lrrecfr ⊢ 𝑅 Fr No
17 16 a1i ⊢ ( ⊤ → 𝑅 Fr No )
18 2 17 17 17 frxp3 ⊢ ( ⊤ → 𝑆 Fr ( ( No × No ) × No ) )
19 18 mptru ⊢ 𝑆 Fr ( ( No × No ) × No )
20 1 lrrecpo ⊢ 𝑅 Po No
21 20 a1i ⊢ ( ⊤ → 𝑅 Po No )
22 2 21 21 21 poxp3 ⊢ ( ⊤ → 𝑆 Po ( ( No × No ) × No ) )
23 22 mptru ⊢ 𝑆 Po ( ( No × No ) × No )
24 1 lrrecse ⊢ 𝑅 Se No
25 24 a1i ⊢ ( ⊤ → 𝑅 Se No )
26 2 25 25 25 sexp3 ⊢ ( ⊤ → 𝑆 Se ( ( No × No ) × No ) )
27 26 mptru ⊢ 𝑆 Se ( ( No × No ) × No )
28 elxpxp ⊢ ( 𝑝 ∈ ( ( No × No ) × No ) ↔ ∃ 𝑥 ∈ No ∃ 𝑦 ∈ No ∃ 𝑧 ∈ No 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
29 2 xpord3pred ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → Pred ( 𝑆 , ( ( No × No ) × No ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) = ( ( ( ( Pred ( 𝑅 , No , 𝑥 ) ∪ { 𝑥 } ) × ( Pred ( 𝑅 , No , 𝑦 ) ∪ { 𝑦 } ) ) × ( Pred ( 𝑅 , No , 𝑧 ) ∪ { 𝑧 } ) ) ∖ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) )
30 1 lrrecpred ⊢ ( 𝑥 ∈ No → Pred ( 𝑅 , No , 𝑥 ) = ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
31 30 3ad2ant1 ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → Pred ( 𝑅 , No , 𝑥 ) = ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
32 31 uneq1d ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( Pred ( 𝑅 , No , 𝑥 ) ∪ { 𝑥 } ) = ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) )
33 1 lrrecpred ⊢ ( 𝑦 ∈ No → Pred ( 𝑅 , No , 𝑦 ) = ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
34 33 3ad2ant2 ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → Pred ( 𝑅 , No , 𝑦 ) = ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
35 34 uneq1d ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( Pred ( 𝑅 , No , 𝑦 ) ∪ { 𝑦 } ) = ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) )
36 32 35 xpeq12d ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ( Pred ( 𝑅 , No , 𝑥 ) ∪ { 𝑥 } ) × ( Pred ( 𝑅 , No , 𝑦 ) ∪ { 𝑦 } ) ) = ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) )
37 1 lrrecpred ⊢ ( 𝑧 ∈ No → Pred ( 𝑅 , No , 𝑧 ) = ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
38 37 3ad2ant3 ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → Pred ( 𝑅 , No , 𝑧 ) = ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) )
39 38 uneq1d ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( Pred ( 𝑅 , No , 𝑧 ) ∪ { 𝑧 } ) = ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) )
40 36 39 xpeq12d ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ( ( Pred ( 𝑅 , No , 𝑥 ) ∪ { 𝑥 } ) × ( Pred ( 𝑅 , No , 𝑦 ) ∪ { 𝑦 } ) ) × ( Pred ( 𝑅 , No , 𝑧 ) ∪ { 𝑧 } ) ) = ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) )
41 40 difeq1d ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ( ( ( Pred ( 𝑅 , No , 𝑥 ) ∪ { 𝑥 } ) × ( Pred ( 𝑅 , No , 𝑦 ) ∪ { 𝑦 } ) ) × ( Pred ( 𝑅 , No , 𝑧 ) ∪ { 𝑧 } ) ) ∖ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) = ( ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∖ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) )
42 29 41 eqtrd ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → Pred ( 𝑆 , ( ( No × No ) × No ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) = ( ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∖ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) )
43 42 raleqdv ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) 𝜓 ↔ ∀ 𝑞 ∈ ( ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∖ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) 𝜓 ) )
44 eldif ⊢ ( 𝑞 ∈ ( ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∖ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) ↔ ( 𝑞 ∈ ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∧ ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) )
45 44 imbi1i ⊢ ( ( 𝑞 ∈ ( ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∖ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) → 𝜓 ) ↔ ( ( 𝑞 ∈ ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∧ ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) → 𝜓 ) )
46 impexp ⊢ ( ( ( 𝑞 ∈ ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∧ ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) → 𝜓 ) ↔ ( 𝑞 ∈ ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) → ( ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } → 𝜓 ) ) )
47 45 46 bitri ⊢ ( ( 𝑞 ∈ ( ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∖ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) → 𝜓 ) ↔ ( 𝑞 ∈ ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) → ( ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } → 𝜓 ) ) )
48 47 ralbii2 ⊢ ( ∀ 𝑞 ∈ ( ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ∖ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) 𝜓 ↔ ∀ 𝑞 ∈ ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ( ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } → 𝜓 ) )
49 43 48 bitrdi ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) 𝜓 ↔ ∀ 𝑞 ∈ ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ( ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } → 𝜓 ) ) )
50 eleq1 ⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ↔ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) )
51 50 notbid ⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ↔ ¬ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ) )
52 df-ne ⊢ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ≠ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ¬ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
53 vex ⊢ 𝑤 ∈ V
54 vex ⊢ 𝑡 ∈ V
55 vex ⊢ 𝑢 ∈ V
56 53 54 55 otthne ⊢ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ≠ ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
57 52 56 bitr3i ⊢ ( ¬ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ↔ ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
58 opex ⊢ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ V
59 58 elsn ⊢ ( ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ↔ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ )
60 57 59 xchnxbir ⊢ ( ¬ ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ↔ ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
61 51 60 bitrdi ⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } ↔ ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ) )
62 61 5 imbi12d ⊢ ( 𝑞 = ⟨ ⟨ 𝑤 , 𝑡 ⟩ , 𝑢 ⟩ → ( ( ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } → 𝜓 ) ↔ ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) )
63 62 ralxp3 ⊢ ( ∀ 𝑞 ∈ ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ( ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } → 𝜓 ) ↔ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
64 ssun1 ⊢ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ⊆ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } )
65 ssralv ⊢ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ⊆ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) → ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) )
66 64 65 ax-mp ⊢ ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
67 ssun1 ⊢ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ⊆ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } )
68 ssralv ⊢ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ⊆ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) → ( ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) )
69 67 68 ax-mp ⊢ ( ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
70 ssun1 ⊢ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ⊆ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } )
71 ssralv ⊢ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ⊆ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) → ( ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) )
72 70 71 ax-mp ⊢ ( ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
73 72 ralimi ⊢ ( ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
74 69 73 syl ⊢ ( ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
75 74 ralimi ⊢ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
76 66 75 syl ⊢ ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
77 76 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
78 nfv ⊢ Ⅎ 𝑤 ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No )
79 nfra1 ⊢ Ⅎ 𝑤 ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 )
80 78 79 nfan ⊢ Ⅎ 𝑤 ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
81 nfv ⊢ Ⅎ 𝑡 ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No )
82 nfra2w ⊢ Ⅎ 𝑡 ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 )
83 81 82 nfan ⊢ Ⅎ 𝑡 ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
84 nfv ⊢ Ⅎ 𝑡 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) )
85 83 84 nfan ⊢ Ⅎ 𝑡 ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
86 nfv ⊢ Ⅎ 𝑢 ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No )
87 nfcv ⊢ Ⅎ 𝑢 ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } )
88 nfra2w ⊢ Ⅎ 𝑢 ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 )
89 87 88 nfralw ⊢ Ⅎ 𝑢 ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 )
90 86 89 nfan ⊢ Ⅎ 𝑢 ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
91 nfv ⊢ Ⅎ 𝑢 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) )
92 90 91 nfan ⊢ Ⅎ 𝑢 ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) )
93 nfv ⊢ Ⅎ 𝑢 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) )
94 92 93 nfan ⊢ Ⅎ 𝑢 ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
95 simpl1 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → 𝑥 ∈ No )
96 leftirr ⊢ ( 𝑥 ∈ No → ¬ 𝑥 ∈ ( L ‘ 𝑥 ) )
97 95 96 syl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ¬ 𝑥 ∈ ( L ‘ 𝑥 ) )
98 rightirr ⊢ ( 𝑥 ∈ No → ¬ 𝑥 ∈ ( R ‘ 𝑥 ) )
99 95 98 syl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ¬ 𝑥 ∈ ( R ‘ 𝑥 ) )
100 ioran ⊢ ( ¬ ( 𝑥 ∈ ( L ‘ 𝑥 ) ∨ 𝑥 ∈ ( R ‘ 𝑥 ) ) ↔ ( ¬ 𝑥 ∈ ( L ‘ 𝑥 ) ∧ ¬ 𝑥 ∈ ( R ‘ 𝑥 ) ) )
101 97 99 100 sylanbrc ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ¬ ( 𝑥 ∈ ( L ‘ 𝑥 ) ∨ 𝑥 ∈ ( R ‘ 𝑥 ) ) )
102 eleq1w ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ↔ 𝑥 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) )
103 elun ⊢ ( 𝑥 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ ( L ‘ 𝑥 ) ∨ 𝑥 ∈ ( R ‘ 𝑥 ) ) )
104 102 103 bitrdi ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ ( L ‘ 𝑥 ) ∨ 𝑥 ∈ ( R ‘ 𝑥 ) ) ) )
105 104 notbid ⊢ ( 𝑤 = 𝑥 → ( ¬ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ↔ ¬ ( 𝑥 ∈ ( L ‘ 𝑥 ) ∨ 𝑥 ∈ ( R ‘ 𝑥 ) ) ) )
106 101 105 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( 𝑤 = 𝑥 → ¬ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) )
107 106 necon2ad ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) → 𝑤 ≠ 𝑥 ) )
108 107 imp ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → 𝑤 ≠ 𝑥 )
109 108 3mix1d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
110 109 adantr ⊢ ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
111 110 adantr ⊢ ( ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
112 pm2.27 ⊢ ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → 𝜃 ) )
113 111 112 syl ⊢ ( ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → 𝜃 ) )
114 94 113 ralimda ⊢ ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → ( ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ) )
115 85 114 ralimda ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ) )
116 80 115 ralimda ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ) )
117 77 116 mpd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 )
118 ssun2 ⊢ { 𝑧 } ⊆ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } )
119 ssralv ⊢ ( { 𝑧 } ⊆ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) → ( ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) )
120 118 119 ax-mp ⊢ ( ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
121 120 ralimi ⊢ ( ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
122 69 121 syl ⊢ ( ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
123 122 ralimi ⊢ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
124 66 123 syl ⊢ ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
125 124 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
126 vex ⊢ 𝑧 ∈ V
127 biidd ⊢ ( 𝑢 = 𝑧 → ( 𝑤 ≠ 𝑥 ↔ 𝑤 ≠ 𝑥 ) )
128 biidd ⊢ ( 𝑢 = 𝑧 → ( 𝑡 ≠ 𝑦 ↔ 𝑡 ≠ 𝑦 ) )
129 neeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ≠ 𝑧 ↔ 𝑧 ≠ 𝑧 ) )
130 127 128 129 3orbi123d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ↔ ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) ) )
131 130 6 imbi12d ⊢ ( 𝑢 = 𝑧 → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜏 ) ) )
132 126 131 ralsn ⊢ ( ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜏 ) )
133 132 2ralbii ⊢ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜏 ) )
134 125 133 sylib ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜏 ) )
135 108 3mix1d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) )
136 135 adantr ⊢ ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) )
137 pm2.27 ⊢ ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜏 ) → 𝜏 ) )
138 136 137 syl ⊢ ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜏 ) → 𝜏 ) )
139 85 138 ralimda ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜏 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 ) )
140 80 139 ralimda ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜏 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 ) )
141 134 140 mpd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 )
142 ssun2 ⊢ { 𝑦 } ⊆ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } )
143 ssralv ⊢ ( { 𝑦 } ⊆ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) → ( ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) )
144 142 143 ax-mp ⊢ ( ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
145 72 ralimi ⊢ ( ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
146 144 145 syl ⊢ ( ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
147 146 ralimi ⊢ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
148 66 147 syl ⊢ ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
149 148 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
150 vex ⊢ 𝑦 ∈ V
151 biidd ⊢ ( 𝑡 = 𝑦 → ( 𝑤 ≠ 𝑥 ↔ 𝑤 ≠ 𝑥 ) )
152 neeq1 ⊢ ( 𝑡 = 𝑦 → ( 𝑡 ≠ 𝑦 ↔ 𝑦 ≠ 𝑦 ) )
153 biidd ⊢ ( 𝑡 = 𝑦 → ( 𝑢 ≠ 𝑧 ↔ 𝑢 ≠ 𝑧 ) )
154 151 152 153 3orbi123d ⊢ ( 𝑡 = 𝑦 → ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ↔ ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ) )
155 154 7 imbi12d ⊢ ( 𝑡 = 𝑦 → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) ) )
156 155 ralbidv ⊢ ( 𝑡 = 𝑦 → ( ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) ) )
157 150 156 ralsn ⊢ ( ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) )
158 157 ralbii ⊢ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) )
159 149 158 sylib ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) )
160 108 3mix1d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
161 160 adantr ⊢ ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
162 pm2.27 ⊢ ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) → 𝜂 ) )
163 161 162 syl ⊢ ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) → 𝜂 ) )
164 92 163 ralimda ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) → ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 ) )
165 80 164 ralimda ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 ) )
166 159 165 mpd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 )
167 117 141 166 3jca ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 ) )
168 120 ralimi ⊢ ( ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
169 144 168 syl ⊢ ( ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
170 169 ralimi ⊢ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
171 66 170 syl ⊢ ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
172 171 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
173 155 ralbidv ⊢ ( 𝑡 = 𝑦 → ( ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) ) )
174 150 173 ralsn ⊢ ( ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) )
175 biidd ⊢ ( 𝑢 = 𝑧 → ( 𝑦 ≠ 𝑦 ↔ 𝑦 ≠ 𝑦 ) )
176 127 175 129 3orbi123d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ↔ ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) ) )
177 176 8 imbi12d ⊢ ( 𝑢 = 𝑧 → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) ↔ ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜁 ) ) )
178 126 177 ralsn ⊢ ( ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜂 ) ↔ ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜁 ) )
179 174 178 bitri ⊢ ( ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜁 ) )
180 179 ralbii ⊢ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜁 ) )
181 172 180 sylib ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜁 ) )
182 108 3mix1d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) )
183 pm2.27 ⊢ ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜁 ) → 𝜁 ) )
184 182 183 syl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ) → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜁 ) → 𝜁 ) )
185 80 184 ralimda ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜁 ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜁 ) )
186 181 185 mpd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜁 )
187 ssun2 ⊢ { 𝑥 } ⊆ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } )
188 ssralv ⊢ ( { 𝑥 } ⊆ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) → ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) )
189 187 188 ax-mp ⊢ ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
190 74 ralimi ⊢ ( ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
191 189 190 syl ⊢ ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
192 191 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
193 vex ⊢ 𝑥 ∈ V
194 neeq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 ≠ 𝑥 ↔ 𝑥 ≠ 𝑥 ) )
195 biidd ⊢ ( 𝑤 = 𝑥 → ( 𝑡 ≠ 𝑦 ↔ 𝑡 ≠ 𝑦 ) )
196 biidd ⊢ ( 𝑤 = 𝑥 → ( 𝑢 ≠ 𝑧 ↔ 𝑢 ≠ 𝑧 ) )
197 194 195 196 3orbi123d ⊢ ( 𝑤 = 𝑥 → ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ↔ ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ) )
198 197 9 imbi12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ) )
199 198 2ralbidv ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ) )
200 193 199 ralsn ⊢ ( ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) )
201 192 200 sylib ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) )
202 90 93 nfan ⊢ Ⅎ 𝑢 ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) )
203 simpl2 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → 𝑦 ∈ No )
204 leftirr ⊢ ( 𝑦 ∈ No → ¬ 𝑦 ∈ ( L ‘ 𝑦 ) )
205 203 204 syl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ¬ 𝑦 ∈ ( L ‘ 𝑦 ) )
206 rightirr ⊢ ( 𝑦 ∈ No → ¬ 𝑦 ∈ ( R ‘ 𝑦 ) )
207 203 206 syl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ¬ 𝑦 ∈ ( R ‘ 𝑦 ) )
208 ioran ⊢ ( ¬ ( 𝑦 ∈ ( L ‘ 𝑦 ) ∨ 𝑦 ∈ ( R ‘ 𝑦 ) ) ↔ ( ¬ 𝑦 ∈ ( L ‘ 𝑦 ) ∧ ¬ 𝑦 ∈ ( R ‘ 𝑦 ) ) )
209 205 207 208 sylanbrc ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ¬ ( 𝑦 ∈ ( L ‘ 𝑦 ) ∨ 𝑦 ∈ ( R ‘ 𝑦 ) ) )
210 eleq1w ⊢ ( 𝑡 = 𝑦 → ( 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ↔ 𝑦 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) )
211 elun ⊢ ( 𝑦 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ↔ ( 𝑦 ∈ ( L ‘ 𝑦 ) ∨ 𝑦 ∈ ( R ‘ 𝑦 ) ) )
212 210 211 bitrdi ⊢ ( 𝑡 = 𝑦 → ( 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ↔ ( 𝑦 ∈ ( L ‘ 𝑦 ) ∨ 𝑦 ∈ ( R ‘ 𝑦 ) ) ) )
213 212 notbid ⊢ ( 𝑡 = 𝑦 → ( ¬ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ↔ ¬ ( 𝑦 ∈ ( L ‘ 𝑦 ) ∨ 𝑦 ∈ ( R ‘ 𝑦 ) ) ) )
214 209 213 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( 𝑡 = 𝑦 → ¬ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) )
215 214 necon2ad ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) → 𝑡 ≠ 𝑦 ) )
216 215 imp ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → 𝑡 ≠ 𝑦 )
217 216 adantr ⊢ ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → 𝑡 ≠ 𝑦 )
218 217 3mix2d ⊢ ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
219 pm2.27 ⊢ ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → ( ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) → 𝜎 ) )
220 218 219 syl ⊢ ( ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → ( ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) → 𝜎 ) )
221 202 220 ralimda ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → ( ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) → ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 ) )
222 83 221 ralimda ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 ) )
223 201 222 mpd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 )
224 122 ralimi ⊢ ( ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
225 189 224 syl ⊢ ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
226 225 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
227 198 2ralbidv ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ) )
228 193 227 ralsn ⊢ ( ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) )
229 biidd ⊢ ( 𝑢 = 𝑧 → ( 𝑥 ≠ 𝑥 ↔ 𝑥 ≠ 𝑥 ) )
230 229 128 129 3orbi123d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ↔ ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) ) )
231 230 10 imbi12d ⊢ ( 𝑢 = 𝑧 → ( ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ↔ ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜌 ) ) )
232 126 231 ralsn ⊢ ( ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ↔ ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜌 ) )
233 232 ralbii ⊢ ( ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ↔ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜌 ) )
234 228 233 bitri ⊢ ( ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ { 𝑧 } ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜌 ) )
235 226 234 sylib ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜌 ) )
236 216 3mix2d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) )
237 pm2.27 ⊢ ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → ( ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜌 ) → 𝜌 ) )
238 236 237 syl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ) → ( ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜌 ) → 𝜌 ) )
239 83 238 ralimda ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑧 ≠ 𝑧 ) → 𝜌 ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜌 ) )
240 235 239 mpd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜌 )
241 186 223 240 3jca ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜁 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜌 ) )
242 146 ralimi ⊢ ( ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
243 189 242 syl ⊢ ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
244 243 adantl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) )
245 198 2ralbidv ⊢ ( 𝑤 = 𝑥 → ( ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ) )
246 193 245 ralsn ⊢ ( ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) )
247 biidd ⊢ ( 𝑡 = 𝑦 → ( 𝑥 ≠ 𝑥 ↔ 𝑥 ≠ 𝑥 ) )
248 247 152 153 3orbi123d ⊢ ( 𝑡 = 𝑦 → ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ↔ ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) ) )
249 248 11 imbi12d ⊢ ( 𝑡 = 𝑦 → ( ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ↔ ( ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜇 ) ) )
250 249 ralbidv ⊢ ( 𝑡 = 𝑦 → ( ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ↔ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜇 ) ) )
251 150 250 ralsn ⊢ ( ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜎 ) ↔ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜇 ) )
252 246 251 bitri ⊢ ( ∀ 𝑤 ∈ { 𝑥 } ∀ 𝑡 ∈ { 𝑦 } ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ↔ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜇 ) )
253 244 252 sylib ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜇 ) )
254 simpl3 ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → 𝑧 ∈ No )
255 leftirr ⊢ ( 𝑧 ∈ No → ¬ 𝑧 ∈ ( L ‘ 𝑧 ) )
256 254 255 syl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ¬ 𝑧 ∈ ( L ‘ 𝑧 ) )
257 rightirr ⊢ ( 𝑧 ∈ No → ¬ 𝑧 ∈ ( R ‘ 𝑧 ) )
258 254 257 syl ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ¬ 𝑧 ∈ ( R ‘ 𝑧 ) )
259 ioran ⊢ ( ¬ ( 𝑧 ∈ ( L ‘ 𝑧 ) ∨ 𝑧 ∈ ( R ‘ 𝑧 ) ) ↔ ( ¬ 𝑧 ∈ ( L ‘ 𝑧 ) ∧ ¬ 𝑧 ∈ ( R ‘ 𝑧 ) ) )
260 256 258 259 sylanbrc ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ¬ ( 𝑧 ∈ ( L ‘ 𝑧 ) ∨ 𝑧 ∈ ( R ‘ 𝑧 ) ) )
261 eleq1w ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ↔ 𝑧 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) )
262 elun ⊢ ( 𝑧 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ↔ ( 𝑧 ∈ ( L ‘ 𝑧 ) ∨ 𝑧 ∈ ( R ‘ 𝑧 ) ) )
263 261 262 bitrdi ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ↔ ( 𝑧 ∈ ( L ‘ 𝑧 ) ∨ 𝑧 ∈ ( R ‘ 𝑧 ) ) ) )
264 263 notbid ⊢ ( 𝑢 = 𝑧 → ( ¬ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ↔ ¬ ( 𝑧 ∈ ( L ‘ 𝑧 ) ∨ 𝑧 ∈ ( R ‘ 𝑧 ) ) ) )
265 260 264 syl5ibrcom ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( 𝑢 = 𝑧 → ¬ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) )
266 265 necon2ad ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) → 𝑢 ≠ 𝑧 ) )
267 266 imp ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → 𝑢 ≠ 𝑧 )
268 267 3mix3d ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) )
269 pm2.27 ⊢ ( ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → ( ( ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜇 ) → 𝜇 ) )
270 268 269 syl ⊢ ( ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) ∧ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ) → ( ( ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜇 ) → 𝜇 ) )
271 90 270 ralimda ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ( ( 𝑥 ≠ 𝑥 ∨ 𝑦 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜇 ) → ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜇 ) )
272 253 271 mpd ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜇 )
273 167 241 272 3jca ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) ∧ ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) ) → ( ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 ) ∧ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜁 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜌 ) ∧ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜇 ) )
274 273 ex ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → ( ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜃 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜏 ∧ ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜂 ) ∧ ( ∀ 𝑤 ∈ ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) 𝜁 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜎 ∧ ∀ 𝑡 ∈ ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) 𝜌 ) ∧ ∀ 𝑢 ∈ ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) 𝜇 ) ) )
275 274 15 syld ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ∀ 𝑤 ∈ ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) ∀ 𝑡 ∈ ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ∀ 𝑢 ∈ ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ( ( 𝑤 ≠ 𝑥 ∨ 𝑡 ≠ 𝑦 ∨ 𝑢 ≠ 𝑧 ) → 𝜃 ) → 𝜒 ) )
276 63 275 syl5bi ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ∀ 𝑞 ∈ ( ( ( ( ( L ‘ 𝑥 ) ∪ ( R ‘ 𝑥 ) ) ∪ { 𝑥 } ) × ( ( ( L ‘ 𝑦 ) ∪ ( R ‘ 𝑦 ) ) ∪ { 𝑦 } ) ) × ( ( ( L ‘ 𝑧 ) ∪ ( R ‘ 𝑧 ) ) ∪ { 𝑧 } ) ) ( ¬ 𝑞 ∈ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ } → 𝜓 ) → 𝜒 ) )
277 49 276 sylbid ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) 𝜓 → 𝜒 ) )
278 predeq3 ⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → Pred ( 𝑆 , ( ( No × No ) × No ) , 𝑝 ) = Pred ( 𝑆 , ( ( No × No ) × No ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) )
279 278 raleqdv ⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , 𝑝 ) 𝜓 ↔ ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) 𝜓 ) )
280 279 4 imbi12d ⊢ ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , 𝑝 ) 𝜓 → 𝜑 ) ↔ ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ) 𝜓 → 𝜒 ) ) )
281 277 280 syl5ibrcom ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ∧ 𝑧 ∈ No ) → ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , 𝑝 ) 𝜓 → 𝜑 ) ) )
282 281 3expa ⊢ ( ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ) → ( 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , 𝑝 ) 𝜓 → 𝜑 ) ) )
283 282 rexlimdva ⊢ ( ( 𝑥 ∈ No ∧ 𝑦 ∈ No ) → ( ∃ 𝑧 ∈ No 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , 𝑝 ) 𝜓 → 𝜑 ) ) )
284 283 rexlimivv ⊢ ( ∃ 𝑥 ∈ No ∃ 𝑦 ∈ No ∃ 𝑧 ∈ No 𝑝 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ → ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , 𝑝 ) 𝜓 → 𝜑 ) )
285 28 284 sylbi ⊢ ( 𝑝 ∈ ( ( No × No ) × No ) → ( ∀ 𝑞 ∈ Pred ( 𝑆 , ( ( No × No ) × No ) , 𝑝 ) 𝜓 → 𝜑 ) )
286 285 3 frpoins2g ⊢ ( ( 𝑆 Fr ( ( No × No ) × No ) ∧ 𝑆 Po ( ( No × No ) × No ) ∧ 𝑆 Se ( ( No × No ) × No ) ) → ∀ 𝑝 ∈ ( ( No × No ) × No ) 𝜑 )
287 19 23 27 286 mp3an ⊢ ∀ 𝑝 ∈ ( ( No × No ) × No ) 𝜑
288 4 ralxp3 ⊢ ( ∀ 𝑝 ∈ ( ( No × No ) × No ) 𝜑 ↔ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No 𝜒 )
289 287 288 mpbi ⊢ ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No 𝜒
290 12 13 14 rspc3v ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → ( ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No 𝜒 → 𝛻 ) )
291 289 290 mpi ⊢ ( ( 𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝛻 )