Theorem mpobi123f 36320

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

Hypotheses

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

Assertion

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

Distinct variable group:   𝑥,𝑦

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

Proof of Theorem mpobi123f

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		mpobi123f.1	. . . . . . . 8 ⊢ Ⅎ𝑥𝐴
2		mpobi123f.2	. . . . . . . 8 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfeq 2920	. . . . . . 7 ⊢ Ⅎ𝑥 𝐴 = 𝐵
4		eleq2 2827	. . . . . . 7 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
5	3, 4	alrimi 2206	. . . . . 6 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
6		mpobi123f.3	. . . . . . . . 9 ⊢ Ⅎ𝑦𝐴
7	6	nfcri 2894	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
8		mpobi123f.4	. . . . . . . . 9 ⊢ Ⅎ𝑦𝐵
9	8	nfcri 2894	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐵
10	7, 9	nfbi 1906	. . . . . . 7 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
11		ax-5 1913	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
12	10, 11	alrimi 2206	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
13	5, 12	sylg 1825	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
14		mpobi123f.5	. . . . . . . 8 ⊢ Ⅎ𝑦𝐶
15		mpobi123f.6	. . . . . . . 8 ⊢ Ⅎ𝑦𝐷
16	14, 15	nfeq 2920	. . . . . . 7 ⊢ Ⅎ𝑦 𝐶 = 𝐷
17		eleq2 2827	. . . . . . 7 ⊢ (𝐶 = 𝐷 → (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
18	16, 17	alrimi 2206	. . . . . 6 ⊢ (𝐶 = 𝐷 → ∀𝑦(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
19		ax-5 1913	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
20	19	alimi 1814	. . . . . 6 ⊢ (∀𝑦(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
21		mpobi123f.7	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝐶
22	21	nfcri 2894	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐶
23		mpobi123f.8	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝐷
24	23	nfcri 2894	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐷
25	22, 24	nfbi 1906	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)
26	25	nfal 2317	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)
27	26	nfal 2317	. . . . . . 7 ⊢ Ⅎ𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)
28	27	nf5ri 2188	. . . . . 6 ⊢ (∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ∀𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
29	18, 20, 28	3syl 18	. . . . 5 ⊢ (𝐶 = 𝐷 → ∀𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
30		id 22	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
31	30	alanimi 1819	. . . . . . 7 ⊢ ((∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ ∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
32	31	alanimi 1819	. . . . . 6 ⊢ ((∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ ∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
33	32	alanimi 1819	. . . . 5 ⊢ ((∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ ∀𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
34	13, 29, 33	syl2an 596	. . . 4 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
35		eqeq2 2750	. . . . . . 7 ⊢ (𝐸 = 𝐹 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
36	35	alrimiv 1930	. . . . . 6 ⊢ (𝐸 = 𝐹 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
37	36	2ralimi 3088	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
38		hbra1 3145	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑦∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
39		rsp 3131	. . . . . . . . 9 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → (𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
40	38, 39	alrimih 1826	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑦(𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
41		19.21v 1942	. . . . . . . . 9 ⊢ (∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ↔ (𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
42	41	albii 1822	. . . . . . . 8 ⊢ (∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
43	40, 42	sylibr 233	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
44	43	ralimi 3087	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
45		hbra1 3145	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) → ∀𝑥∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
46		rsp 3131	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) → (𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
47	45, 46	alrimih 1826	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) → ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
48		19.21v 1942	. . . . . . . 8 ⊢ (∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
49	48	2albii 1823	. . . . . . 7 ⊢ (∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
50	7	19.21 2200	. . . . . . . 8 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ (𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
51	50	albii 1822	. . . . . . 7 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
52	49, 51	sylbbr 235	. . . . . 6 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
53	44, 47, 52	3syl 18	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
54	37, 53	syl 17	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹 → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
55		id 22	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
56	55	alanimi 1819	. . . . . 6 ⊢ ((∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ ∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
57	56	alanimi 1819	. . . . 5 ⊢ ((∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ ∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
58	57	alanimi 1819	. . . 4 ⊢ ((∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
59	34, 54, 58	syl2an 596	. . 3 ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → ∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
60		tsan2 36300	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑥 ∈ 𝐴 ∨ ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
61	60	ord 861	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
62		tsan2 36300	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
63	62	a1d 25	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
64	61, 63	cnf1dd 36248	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
65		tsbi2 36292	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
66	65	ord 861	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
67	66	a1dd 50	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
68		ax-1 6	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
69	67, 68	contrd 36255	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
70	69	a1d 25	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
71	64, 70	cnf1dd 36248	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
72		idd 24	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐴))
73		tsan2 36300	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∨ ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
74	73	ord 861	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
75		tsan2 36300	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
76	75	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
77	74, 76	cnf1dd 36248	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
78		tsim2 36289	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
79	78	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
80	77, 79	cnf1dd 36248	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
81		ax-1 6	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
82	80, 81	contrd 36255	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
83	82	a1d 25	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
84		tsbi3 36293	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵) ∨ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
85	84	a1d 25	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵) ∨ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))))
86	83, 85	cnfn2dd 36251	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵)))
87	72, 86	cnf1dd 36248	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
88		tsan2 36300	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑥 ∈ 𝐵 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
89	88	a1d 25	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))))
90	87, 89	cnf1dd 36248	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
91		tsan2 36300	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
92	91	a1d 25	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
93	90, 92	cnf1dd 36248	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
94	71, 93	contrd 36255	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → 𝑥 ∈ 𝐴)
95	94	a1d 25	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥 ∈ 𝐴))
96		ax-1 6	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
97	78	a1d 25	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
98	96, 97	cnf2dd 36249	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
99		tsan3 36301	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
100	99	a1d 25	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
101	98, 100	cnfn2dd 36251	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
102	95, 101	mpdd 43	. . . . . . 7 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
103		notnotr 130	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))
104	103	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
105	91	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
106	104, 105	cnfn2dd 36251	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
107		tsan3 36301	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑦 ∈ 𝐷 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
108	107	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑦 ∈ 𝐷 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))))
109	106, 108	cnfn2dd 36251	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑦 ∈ 𝐷))
110		tsan3 36301	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
111	110	ord 861	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
112	75	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
113	111, 112	cnf1dd 36248	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
114	78	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
115	113, 114	cnf1dd 36248	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
116		ax-1 6	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
117	115, 116	contrd 36255	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
118	109, 117	sylibrd 258	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑦 ∈ 𝐶))
119	94	a1d 25	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑥 ∈ 𝐴))
120		ax-1 6	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
121	78	a1d 25	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
122	120, 121	cnf2dd 36249	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
123	99	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
124	122, 123	cnfn2dd 36251	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
125	119, 124	mpdd 43	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
126	118, 125	mpdd 43	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
127	119, 118	jcad 513	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
128		tsim3 36290	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
129	128	a1d 25	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
130	120, 129	cnf2dd 36249	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
131		tsbi1 36291	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
132	131	a1d 25	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
133	130, 132	cnf2dd 36249	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
134	104, 133	cnfn2dd 36251	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
135		tsan1 36299	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
136	135	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
137	134, 136	cnf2dd 36249	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ 𝑧 = 𝐸)))
138	127, 137	cnfn1dd 36250	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ 𝑧 = 𝐸))
139		tsan3 36301	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐹 ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
140	139	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐹 ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
141	104, 140	cnfn2dd 36251	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑧 = 𝐹))
142		tsbi3 36293	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
143	142	a1d 25	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
144	143	or32dd 36252	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ ¬ 𝑧 = 𝐹)))
145	141, 144	cnfn2dd 36251	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
146	138, 145	cnf1dd 36248	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
147	126, 146	contrd 36255	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))
148	147	a1d 25	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
149	128	a1d 25	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
150	96, 149	cnf2dd 36249	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
151	65	a1d 25	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
152	150, 151	cnf2dd 36249	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
153	148, 152	cnf2dd 36249	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
154	62	a1d 25	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
155	153, 154	cnfn2dd 36251	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
156		tsan3 36301	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑦 ∈ 𝐶 ∨ ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
157	156	a1d 25	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦 ∈ 𝐶 ∨ ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))))
158	155, 157	cnfn2dd 36251	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦 ∈ 𝐶))
159		tsan3 36301	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐸 ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
160	159	a1d 25	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑧 = 𝐸 ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
161	153, 160	cnfn2dd 36251	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑧 = 𝐸))
162	95, 82	sylibd 238	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥 ∈ 𝐵))
163	158, 117	sylibd 238	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦 ∈ 𝐷))
164	162, 163	jcad 513	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
165		tsan1 36299	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
166	165	a1d 25	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
167	148, 166	cnf2dd 36249	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ 𝑧 = 𝐹)))
168	164, 167	cnfn1dd 36250	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ 𝑧 = 𝐹))
169		tsbi4 36294	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
170	169	a1d 25	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
171	170	or32dd 36252	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ 𝑧 = 𝐹)))
172	168, 171	cnf2dd 36249	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
173	161, 172	cnfn1dd 36250	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
174		tsim1 36288	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑦 ∈ 𝐶 ∨ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
175	174	a1d 25	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦 ∈ 𝐶 ∨ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
176	175	or32dd 36252	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦 ∈ 𝐶 ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
177	173, 176	cnf2dd 36249	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑦 ∈ 𝐶 ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
178	158, 177	cnfn1dd 36250	. . . . . . 7 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
179	102, 178	contrd 36255	. . . . . 6 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ⊥)
180	179	efald2 36236	. . . . 5 ⊢ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
181	180	alimi 1814	. . . 4 ⊢ (∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
182	181	2alimi 1815	. . 3 ⊢ (∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
183		oprabbi 36319	. . 3 ⊢ (∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)})
184	59, 182, 183	3syl 18	. 2 ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)})
185		df-mpo 7280	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)}
186		df-mpo 7280	. 2 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)}
187	184, 185, 186	3eqtr4g 2803	1 ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844  ∀wal 1537   = wceq 1539  ⊥wfal 1551   ∈ wcel 2106  Ⅎwnfc 2887  ∀wral 3064  {coprab 7276   ∈ cmpo 7277

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-13 2372  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-oprab 7279  df-mpo 7280

This theorem is referenced by: (None)