no3indslem

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

	Ref	Expression
Hypotheses	no3indslem.a	$⊢ R = \{⟨a, b⟩ \| a \in (L (b) \cup R (b))\}$
	no3indslem.b	$⊢ S = \{⟨c, d⟩ \| (c \in ((No \times No) \times No) \land d \in ((No \times No) \times No) \land (((1^{st} (1^{st} (c)) R 1^{st} (1^{st} (d)) \lor 1^{st} (1^{st} (c)) = 1^{st} (1^{st} (d))) \land (2^{nd} (1^{st} (c)) R 2^{nd} (1^{st} (d)) \lor 2^{nd} (1^{st} (c)) = 2^{nd} (1^{st} (d))) \land (2^{nd} (c) R 2^{nd} (d) \lor 2^{nd} (c) = 2^{nd} (d))) \land c \neq d))\}$
	no3indslem.1	$⊢ p = q \to (φ \leftrightarrow ψ)$
	no3indslem.2	$⊢ p = ⟨⟨x, y⟩, z⟩ \to (φ \leftrightarrow χ)$
	no3indslem.3	$⊢ q = ⟨⟨w, t⟩, u⟩ \to (ψ \leftrightarrow θ)$
	no3indslem.4	$⊢ u = z \to (θ \leftrightarrow τ)$
	no3indslem.5	$⊢ t = y \to (θ \leftrightarrow η)$
	no3indslem.6	$⊢ u = z \to (η \leftrightarrow ζ)$
	no3indslem.7	$⊢ w = x \to (θ \leftrightarrow σ)$
	no3indslem.8	$⊢ u = z \to (σ \leftrightarrow ρ)$
	no3indslem.9	$⊢ t = y \to (σ \leftrightarrow μ)$
	no3indslem.10	$⊢ x = A \to (χ \leftrightarrow λ)$
	no3indslem.11	$⊢ y = B \to (λ \leftrightarrow κ)$
	no3indslem.12	No typesetting found for \|- ( z = C -> ( ka <-> al ) ) with typecode \|-
	no3indslem.i	$⊢ (x \in No \land y \in No \land z \in No) \to (((\forall w \in (L (x) \cup R (x)) \forall t \in (L (y) \cup R (y)) \forall u \in (L (z) \cup R (z)) θ \land \forall w \in (L (x) \cup R (x)) \forall t \in (L (y) \cup R (y)) τ \land \forall w \in (L (x) \cup R (x)) \forall u \in (L (z) \cup R (z)) η) \land (\forall w \in (L (x) \cup R (x)) ζ \land \forall t \in (L (y) \cup R (y)) \forall u \in (L (z) \cup R (z)) σ \land \forall t \in (L (y) \cup R (y)) ρ) \land \forall u \in (L (z) \cup R (z)) μ) \to χ)$
Assertion	no3indslem	Could not format assertion : No typesetting found for \|- ( ( A e. No /\ B e. No /\ C e. No ) -> al ) with typecode \|-

Proof

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

Metamath Proof Explorer

Theorem no3indslem

Proof