no3indslem - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > no3indslem		Structured version Visualization version GIF version

Theorem no3indslem 33697

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

**Hypotheses**
Ref	Expression
no3indslem.a	⊢ 𝑅 = {⟨𝑎, 𝑏⟩ ∣ 𝑎 ∈ (( L ‘𝑏) ∪ ( R ‘𝑏))}
no3indslem.b	⊢ 𝑆 = {⟨𝑐, 𝑑⟩ ∣ (𝑐 ∈ (( No × No ) × No ) ∧ 𝑑 ∈ (( No × No ) × No ) ∧ ((((1^st ‘(1^st ‘𝑐))𝑅(1^st ‘(1^st ‘𝑑)) ∨ (1^st ‘(1^st ‘𝑐)) = (1^st ‘(1^st ‘𝑑))) ∧ ((2^nd ‘(1^st ‘𝑐))𝑅(2^nd ‘(1^st ‘𝑑)) ∨ (2^nd ‘(1^st ‘𝑐)) = (2^nd ‘(1^st ‘𝑑))) ∧ ((2^nd ‘𝑐)𝑅(2^nd ‘𝑑) ∨ (2^nd ‘𝑐) = (2^nd ‘𝑑))) ∧ 𝑐 ≠ 𝑑))}
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**
Ref	Expression
no3indslem	⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐶 ∈ No ) → 𝛻)

Distinct variable groups: 𝑎,𝑏,𝑥 𝑥,𝐴 𝑦,𝑎 𝑦,𝐴 𝑧,𝑎 𝑧,𝐴 𝑧,𝛻 𝑥,𝑏,𝑦 𝑦,𝐵 𝑧,𝑏 𝑧,𝐵 𝑐,𝑑 𝑧,𝐶 𝜒,𝑝 𝜅,𝑦 𝜆,𝑥 𝜓,𝑝 𝑞,𝑝,𝑥,𝑦,𝑧 𝜑,𝑞,𝑥,𝑦,𝑧 𝜓,𝑡,𝑢,𝑤,𝑥,𝑦,𝑧 𝑡,𝑞 𝜃,𝑞,𝑢 𝑤,𝑞,𝑥,𝑦,𝑧 𝑅,𝑐,𝑑 𝑆,𝑝,𝑞,𝑥,𝑦,𝑧 𝑢,𝑡,𝑤,𝑥,𝑦,𝑧 𝜇,𝑡 𝜎,𝑤 𝜂,𝑡 𝜌,𝑢 𝜏,𝑢 𝜃,𝑢 𝜁,𝑢 Allowed substitution hints: 𝜑(𝑤,𝑢,𝑡,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜓(𝑞,𝑎,𝑏,𝑐,𝑑) 𝜒(𝑥,𝑦,𝑧,𝑤,𝑢,𝑡,𝑞,𝑎,𝑏,𝑐,𝑑) 𝜃(𝑥,𝑦,𝑧,𝑤,𝑡,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜏(𝑥,𝑦,𝑧,𝑤,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜂(𝑥,𝑦,𝑧,𝑤,𝑢,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜁(𝑥,𝑦,𝑧,𝑤,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜎(𝑥,𝑦,𝑧,𝑢,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜌(𝑥,𝑦,𝑧,𝑤,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜇(𝑥,𝑦,𝑧,𝑤,𝑢,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜆(𝑦,𝑧,𝑤,𝑢,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜅(𝑥,𝑧,𝑤,𝑢,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝐴(𝑤,𝑢,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝐵(𝑥,𝑤,𝑢,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝐶(𝑥,𝑦,𝑤,𝑢,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝑅(𝑥,𝑦,𝑧,𝑤,𝑢,𝑡,𝑞,𝑝,𝑎,𝑏) 𝑆(𝑤,𝑢,𝑡,𝑎,𝑏,𝑐,𝑑) 𝛻(𝑥,𝑦,𝑤,𝑢,𝑡,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑)

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

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 399 ∨ wo 844 ∨ w3o 1083 ∧ w3a 1084 = wceq 1538 ⊤wtru 1539 ∈ wcel 2111 ≠ wne 2951 ∀wral 3070 ∃wrex 3071 ∖ cdif 3857 ∪ cun 3858 ⊆ wss 3860 {csn 4525 ⟨cop 4531 class class class wbr 5036 {copab 5098 Po wpo 5445 Fr wfr 5484 Se wse 5485 × cxp 5526 Predcpred 6130 ‘cfv 6340 1^st c1st 7697 2^nd c2nd 7698 No csur 33440 L cleft 33623 R cright 33624

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2729 ax-rep 5160 ax-sep 5173 ax-nul 5180 ax-pow 5238 ax-pr 5302 ax-un 7465

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3or 1085 df-3an 1086 df-tru 1541 df-fal 1551 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2557 df-eu 2588 df-clab 2736 df-cleq 2750 df-clel 2830 df-nfc 2901 df-ne 2952 df-ral 3075 df-rex 3076 df-reu 3077 df-rmo 3078 df-rab 3079 df-v 3411 df-sbc 3699 df-csb 3808 df-dif 3863 df-un 3865 df-in 3867 df-ss 3877 df-pss 3879 df-nul 4228 df-if 4424 df-pw 4499 df-sn 4526 df-pr 4528 df-tp 4530 df-op 4532 df-uni 4802 df-int 4842 df-iun 4888 df-br 5037 df-opab 5099 df-mpt 5117 df-tr 5143 df-id 5434 df-eprel 5439 df-po 5447 df-so 5448 df-fr 5487 df-se 5488 df-we 5489 df-xp 5534 df-rel 5535 df-cnv 5536 df-co 5537 df-dm 5538 df-rn 5539 df-res 5540 df-ima 5541 df-pred 6131 df-ord 6177 df-on 6178 df-suc 6180 df-iota 6299 df-fun 6342 df-fn 6343 df-f 6344 df-f1 6345 df-fo 6346 df-f1o 6347 df-fv 6348 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-1st 7699 df-2nd 7700 df-wrecs 7963 df-recs 8024 df-1o 8118 df-2o 8119 df-no 33443 df-slt 33444 df-bday 33445 df-sslt 33573 df-scut 33575 df-made 33625 df-old 33626 df-left 33628 df-right 33629

This theorem is referenced by: no3inds 33698

W3C validator