Theorem mpt2bi123f 33971

Description: Equality deduction for maps-to notations with two arguments. (Contributed by Giovanni Mascellani, 10-Apr-2018.)

Hypotheses

Ref	Expression
mpt2bi123f.1	⊢ Ⅎ𝑥𝐴
mpt2bi123f.2	⊢ Ⅎ𝑥𝐵
mpt2bi123f.3	⊢ Ⅎ𝑦𝐴
mpt2bi123f.4	⊢ Ⅎ𝑦𝐵
mpt2bi123f.5	⊢ Ⅎ𝑦𝐶
mpt2bi123f.6	⊢ Ⅎ𝑦𝐷
mpt2bi123f.7	⊢ Ⅎ𝑥𝐶
mpt2bi123f.8	⊢ Ⅎ𝑥𝐷

Assertion

Ref	Expression
mpt2bi123f	⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝐴(𝑥,𝑦)   𝐵(𝑥,𝑦)   𝐶(𝑥,𝑦)   𝐷(𝑥,𝑦)   𝐸(𝑥,𝑦)   𝐹(𝑥,𝑦)

Proof of Theorem mpt2bi123f

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpt2bi123f.1	. . . . . . . 8 ⊢ Ⅎ𝑥𝐴
2		mpt2bi123f.2	. . . . . . . 8 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2776	. . . . . . 7 ⊢ Ⅎ𝑥 𝐴 = 𝐵
4		eleq2 2690	. . . . . . 7 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
5	3, 4	alrimi 2082	. . . . . 6 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
6		mpt2bi123f.3	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐴
7	6	nfcri 2758	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
8		mpt2bi123f.4	. . . . . . . . . 10 ⊢ Ⅎ𝑦𝐵
9	8	nfcri 2758	. . . . . . . . 9 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐵
10	7, 9	nfbi 1833	. . . . . . . 8 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
11		ax-5 1839	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
12	10, 11	alrimi 2082	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
13	12	alimi 1739	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
14	5, 13	syl 17	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
15		mpt2bi123f.5	. . . . . . . 8 ⊢ Ⅎ𝑦𝐶
16		mpt2bi123f.6	. . . . . . . 8 ⊢ Ⅎ𝑦𝐷
17	15, 16	nfeq 2776	. . . . . . 7 ⊢ Ⅎ𝑦 𝐶 = 𝐷
18		eleq2 2690	. . . . . . 7 ⊢ (𝐶 = 𝐷 → (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
19	17, 18	alrimi 2082	. . . . . 6 ⊢ (𝐶 = 𝐷 → ∀𝑦(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
20		ax-5 1839	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
21	20	alimi 1739	. . . . . 6 ⊢ (∀𝑦(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
22		mpt2bi123f.7	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝐶
23	22	nfcri 2758	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐶
24		mpt2bi123f.8	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝐷
25	24	nfcri 2758	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐷
26	23, 25	nfbi 1833	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)
27	26	nfal 2153	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)
28	27	nfal 2153	. . . . . . 7 ⊢ Ⅎ𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)
29	28	nf5ri 2065	. . . . . 6 ⊢ (∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ∀𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
30	19, 21, 29	3syl 18	. . . . 5 ⊢ (𝐶 = 𝐷 → ∀𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
31		id 22	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
32	31	alanimi 1744	. . . . . . 7 ⊢ ((∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ ∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
33	32	alanimi 1744	. . . . . 6 ⊢ ((∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ ∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
34	33	alanimi 1744	. . . . 5 ⊢ ((∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ ∀𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
35	14, 30, 34	syl2an 494	. . . 4 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
36		eqeq2 2633	. . . . . . 7 ⊢ (𝐸 = 𝐹 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
37	36	alrimiv 1855	. . . . . 6 ⊢ (𝐸 = 𝐹 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
38	37	2ralimi 2953	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
39		hbra1 2942	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑦∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
40		rsp 2929	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → (𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
41	39, 40	alrimih 1751	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑦(𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
42		19.21v 1868	. . . . . . . . 9 ⊢ (∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ↔ (𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
43	42	albii 1747	. . . . . . . 8 ⊢ (∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
44	41, 43	sylibr 224	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
45	44	ralimi 2952	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
46		hbra1 2942	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) → ∀𝑥∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
47		rsp 2929	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) → (𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
48	46, 47	alrimih 1751	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) → ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
49		19.21v 1868	. . . . . . . 8 ⊢ (∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
50	49	2albii 1748	. . . . . . 7 ⊢ (∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
51	7	19.21 2075	. . . . . . . 8 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ (𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
52	51	albii 1747	. . . . . . 7 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
53	50, 52	sylbbr 226	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
54	45, 48, 53	3syl 18	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
55	38, 54	syl 17	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹 → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
56		id 22	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
57	56	alanimi 1744	. . . . . 6 ⊢ ((∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ ∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
58	57	alanimi 1744	. . . . 5 ⊢ ((∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ ∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
59	58	alanimi 1744	. . . 4 ⊢ ((∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
60	35, 55, 59	syl2an 494	. . 3 ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → ∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
61		tsan2 33949	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑥 ∈ 𝐴 ∨ ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
62	61	ord 392	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
63		tsan2 33949	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
64	63	a1d 25	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
65	62, 64	cnf1dd 33892	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
66		tsbi2 33941	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
67	66	ord 392	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
68	67	a1dd 50	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
69		ax-1 6	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
70	68, 69	contrd 33899	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
71	70	a1d 25	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
72	65, 71	cnf1dd 33892	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
73		idd 24	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐴))
74		tsan2 33949	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∨ ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
75	74	ord 392	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
76		tsan2 33949	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
77	76	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
78	75, 77	cnf1dd 33892	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
79		tsim2 33938	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
80	79	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
81	78, 80	cnf1dd 33892	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
82		ax-1 6	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
83	81, 82	contrd 33899	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
84	83	a1d 25	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
85		tsbi3 33942	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵) ∨ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
86	85	a1d 25	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵) ∨ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))))
87	84, 86	cnfn2dd 33895	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵)))
88	73, 87	cnf1dd 33892	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
89		tsan2 33949	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑥 ∈ 𝐵 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
90	89	a1d 25	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))))
91	88, 90	cnf1dd 33892	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
92		tsan2 33949	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
93	92	a1d 25	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
94	91, 93	cnf1dd 33892	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
95	72, 94	contrd 33899	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → 𝑥 ∈ 𝐴)
96	95	a1d 25	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥 ∈ 𝐴))
97		ax-1 6	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
98	79	a1d 25	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
99	97, 98	cnf2dd 33893	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
100		tsan3 33950	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
101	100	a1d 25	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
102	99, 101	cnfn2dd 33895	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
103	96, 102	mpdd 43	. . . . . . 7 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
104		notnotr 125	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))
105	104	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
106	92	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
107	105, 106	cnfn2dd 33895	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
108		tsan3 33950	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑦 ∈ 𝐷 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
109	108	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑦 ∈ 𝐷 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))))
110	107, 109	cnfn2dd 33895	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑦 ∈ 𝐷))
111		tsan3 33950	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
112	111	ord 392	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
113	76	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
114	112, 113	cnf1dd 33892	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
115	79	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
116	114, 115	cnf1dd 33892	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
117		ax-1 6	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
118	116, 117	contrd 33899	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
119	110, 118	sylibrd 249	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑦 ∈ 𝐶))
120	95	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑥 ∈ 𝐴))
121		ax-1 6	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
122	79	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
123	121, 122	cnf2dd 33893	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
124	100	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
125	123, 124	cnfn2dd 33895	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
126	120, 125	mpdd 43	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
127	119, 126	mpdd 43	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
128	120, 119	jcad 555	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
129		tsim3 33939	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
130	129	a1d 25	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
131	121, 130	cnf2dd 33893	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
132		tsbi1 33940	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
133	132	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
134	131, 133	cnf2dd 33893	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
135	105, 134	cnfn2dd 33895	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
136		tsan1 33948	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
137	136	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
138	135, 137	cnf2dd 33893	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ 𝑧 = 𝐸)))
139	128, 138	cnfn1dd 33894	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ 𝑧 = 𝐸))
140		tsan3 33950	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐹 ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
141	140	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐹 ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
142	105, 141	cnfn2dd 33895	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑧 = 𝐹))
143		tsbi3 33942	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
144	143	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
145	144	or32dd 33896	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ ¬ 𝑧 = 𝐹)))
146	142, 145	cnfn2dd 33895	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
147	139, 146	cnf1dd 33892	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
148	127, 147	contrd 33899	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))
149	148	a1d 25	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
150	129	a1d 25	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
151	97, 150	cnf2dd 33893	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
152	66	a1d 25	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
153	151, 152	cnf2dd 33893	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
154	149, 153	cnf2dd 33893	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
155	63	a1d 25	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
156	154, 155	cnfn2dd 33895	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
157		tsan3 33950	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑦 ∈ 𝐶 ∨ ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
158	157	a1d 25	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦 ∈ 𝐶 ∨ ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))))
159	156, 158	cnfn2dd 33895	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦 ∈ 𝐶))
160		tsan3 33950	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐸 ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
161	160	a1d 25	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑧 = 𝐸 ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
162	154, 161	cnfn2dd 33895	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑧 = 𝐸))
163	96, 83	sylibd 229	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥 ∈ 𝐵))
164	159, 118	sylibd 229	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦 ∈ 𝐷))
165	163, 164	jcad 555	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
166		tsan1 33948	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
167	166	a1d 25	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
168	149, 167	cnf2dd 33893	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ 𝑧 = 𝐹)))
169	165, 168	cnfn1dd 33894	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ 𝑧 = 𝐹))
170		tsbi4 33943	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
171	170	a1d 25	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
172	171	or32dd 33896	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ 𝑧 = 𝐹)))
173	169, 172	cnf2dd 33893	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
174	162, 173	cnfn1dd 33894	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
175		tsim1 33937	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑦 ∈ 𝐶 ∨ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
176	175	a1d 25	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦 ∈ 𝐶 ∨ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
177	176	or32dd 33896	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦 ∈ 𝐶 ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
178	174, 177	cnf2dd 33893	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑦 ∈ 𝐶 ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
179	159, 178	cnfn1dd 33894	. . . . . . 7 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
180	103, 179	contrd 33899	. . . . . 6 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ⊥)
181	180	efald2 33877	. . . . 5 ⊢ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
182	181	alimi 1739	. . . 4 ⊢ (∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
183	182	2alimi 1740	. . 3 ⊢ (∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
184		oprabbi 33970	. . 3 ⊢ (∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)})
185	60, 183, 184	3syl 18	. 2 ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)})
186		df-mpt2 6655	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)}
187		df-mpt2 6655	. 2 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)}
188	185, 186, 187	3eqtr4g 2681	1 ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384  ∀wal 1481   = wceq 1483  ⊥wfal 1488   ∈ wcel 1990  Ⅎwnfc 2751  ∀wral 2912  {coprab 6651   ↦ cmpt2 6652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-oprab 6654  df-mpt2 6655

This theorem is referenced by: (None)