Theorem mpobi123f 39074

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 2936	. . . . . . 7 ⊢ Ⅎ𝑥 𝐴 = 𝐵
4		eleq2 2850	. . . . . . 7 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
5	3, 4	alrimi 2250	. . . . . 6 ⊢ (𝐴 = 𝐵 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
6		mpobi123f.3	. . . . . . . . 9 ⊢ Ⅎ𝑦𝐴
7	6	nfcri 2915	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐴
8		mpobi123f.4	. . . . . . . . 9 ⊢ Ⅎ𝑦𝐵
9	8	nfcri 2915	. . . . . . . 8 ⊢ Ⅎ𝑦 𝑥 ∈ 𝐵
10	7, 9	nfbi 1936	. . . . . . 7 ⊢ Ⅎ𝑦(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)
11		ax-5 1943	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
12	10, 11	alrimi 2250	. . . . . 6 ⊢ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
13	5, 12	sylg 1856	. . . . 5 ⊢ (𝐴 = 𝐵 → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
14		mpobi123f.5	. . . . . . . 8 ⊢ Ⅎ𝑦𝐶
15		mpobi123f.6	. . . . . . . 8 ⊢ Ⅎ𝑦𝐷
16	14, 15	nfeq 2936	. . . . . . 7 ⊢ Ⅎ𝑦 𝐶 = 𝐷
17		eleq2 2850	. . . . . . 7 ⊢ (𝐶 = 𝐷 → (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
18	16, 17	alrimi 2250	. . . . . 6 ⊢ (𝐶 = 𝐷 → ∀𝑦(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
19		ax-5 1943	. . . . . . 7 ⊢ ((𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
20	19	alimi 1844	. . . . . 6 ⊢ (∀𝑦(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
21		mpobi123f.7	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝐶
22	21	nfcri 2915	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐶
23		mpobi123f.8	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝐷
24	23	nfcri 2915	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐷
25	22, 24	nfbi 1936	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)
26	25	nfal 2354	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)
27	26	nfal 2354	. . . . . . 7 ⊢ Ⅎ𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)
28	27	nf5ri 2232	. . . . . 6 ⊢ (∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ∀𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
29	18, 20, 28	3syl 19	. . . . 5 ⊢ (𝐶 = 𝐷 → ∀𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
30		id 23	. . . . . . . 8 ⊢ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
31	30	alanimi 1849	. . . . . . 7 ⊢ ((∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ ∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
32	31	alanimi 1849	. . . . . 6 ⊢ ((∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ ∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
33	32	alanimi 1849	. . . . 5 ⊢ ((∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ ∀𝑥∀𝑦∀𝑧(𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) → ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
34	13, 29, 33	syl2an 608	. . . 4 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → ∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)))
35		eqeq2 2773	. . . . . . 7 ⊢ (𝐸 = 𝐹 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
36	35	alrimiv 1960	. . . . . 6 ⊢ (𝐸 = 𝐹 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
37	36	2ralimi 3133	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹 → ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
38		hbra1 3300	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑦∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹))
39		rsp 3251	. . . . . . . 8 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → (𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
40	38, 39	alrimih 1857	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑦(𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
41		19.21v 1972	. . . . . . . 8 ⊢ (∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ↔ (𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
42	41	albii 1852	. . . . . . 7 ⊢ (∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ↔ ∀𝑦(𝑦 ∈ 𝐶 → ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
43	40, 42	sylibr 237	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
44	43	ralimi 3100	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 ∀𝑧(𝑧 = 𝐸 ↔ 𝑧 = 𝐹) → ∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
45		hbra1 3300	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) → ∀𝑥∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
46		rsp 3251	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) → (𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
47	45, 46	alrimih 1857	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) → ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
48		19.21v 1972	. . . . . . 7 ⊢ (∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ (𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
49	48	2albii 1853	. . . . . 6 ⊢ (∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ ∀𝑥∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
50	7	19.21 2244	. . . . . . 7 ⊢ (∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ (𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
51	50	albii 1852	. . . . . 6 ⊢ (∀𝑥∀𝑦(𝑥 ∈ 𝐴 → ∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
52	49, 51	sylbbr 239	. . . . 5 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∀𝑦∀𝑧(𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
53	37, 44, 47, 52	4syl 20	. . . 4 ⊢ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹 → ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
54		id 23	. . . . . . 7 ⊢ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
55	54	alanimi 1849	. . . . . 6 ⊢ ((∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ ∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
56	55	alanimi 1849	. . . . 5 ⊢ ((∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ ∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
57	56	alanimi 1849	. . . 4 ⊢ ((∀𝑥∀𝑦∀𝑧((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ ∀𝑥∀𝑦∀𝑧(𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
58	34, 53, 57	syl2an 608	. . 3 ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → ∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
59		tsan2 39054	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑥 ∈ 𝐴 ∨ ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
60	59	ord 878	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
61		tsan2 39054	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
62	61	a1d 26	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
63	60, 62	cnf1dd 39002	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
64		tsbi2 39046	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
65	64	ord 878	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
66	65	a1dd 51	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
67		ax-1 6	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
68	66, 67	contrd 39009	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
69	68	a1d 26	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
70	63, 69	cnf1dd 39002	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
71		idd 25	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐴))
72		tsan2 39054	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∨ ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
73	72	ord 878	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
74		tsan2 39054	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
75	74	a1d 26	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
76	73, 75	cnf1dd 39002	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
77		tsim2 39043	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
78	77	a1d 26	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
79	76, 78	cnf1dd 39002	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
80		ax-1 6	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
81	79, 80	contrd 39009	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))
82	81	a1d 26	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
83		tsbi3 39047	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵) ∨ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)))
84	83	a1d 26	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵) ∨ ¬ (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵))))
85	82, 84	cnfn2dd 39005	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 ∨ ¬ 𝑥 ∈ 𝐵)))
86	71, 85	cnf1dd 39002	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵))
87		tsan2 39054	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑥 ∈ 𝐵 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
88	87	a1d 26	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐵 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))))
89	86, 88	cnf1dd 39002	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
90		tsan2 39054	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
91	90	a1d 26	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
92	89, 91	cnf1dd 39002	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ 𝑥 ∈ 𝐴 → ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
93	70, 92	contrd 39009	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → 𝑥 ∈ 𝐴)
94	93	a1d 26	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥 ∈ 𝐴))
95		ax-1 6	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
96	77	a1d 26	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
97	95, 96	cnf2dd 39003	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
98		tsan3 39055	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
99	98	a1d 26	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
100	97, 99	cnfn2dd 39005	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
101	94, 100	mpdd 44	. . . . . . 7 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
102		notnotr 131	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))
103	102	a1i 11	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
104	90	a1d 26	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
105	103, 104	cnfn2dd 39005	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
106		tsan3 39055	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑦 ∈ 𝐷 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
107	106	a1d 26	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑦 ∈ 𝐷 ∨ ¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷))))
108	105, 107	cnfn2dd 39005	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑦 ∈ 𝐷))
109		tsan3 39055	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) ∨ ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
110	109	ord 878	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ¬ ((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))))
111	74	a1d 26	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
112	110, 111	cnf1dd 39002	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
113	77	a1d 26	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
114	112, 113	cnf1dd 39002	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
115		ax-1 6	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
116	114, 115	contrd 39009	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷))
117	108, 116	sylibrd 262	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑦 ∈ 𝐶))
118	93	a1d 26	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑥 ∈ 𝐴))
119		ax-1 6	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
120	77	a1d 26	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
121	119, 120	cnf2dd 39003	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))))
122	98	a1d 26	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ ¬ (((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))))
123	121, 122	cnfn2dd 39005	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
124	118, 123	mpdd 44	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
125	117, 124	mpdd 44	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
126	118, 117	jcad 522	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
127		tsim3 39044	. . . . . . . . . . . . . . . . . . . 20 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
128	127	a1d 26	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
129	119, 128	cnf2dd 39003	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
130		tsbi1 39045	. . . . . . . . . . . . . . . . . . 19 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
131	130	a1d 26	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
132	129, 131	cnf2dd 39003	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
133	103, 132	cnfn2dd 39005	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
134		tsan1 39053	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
135	134	a1d 26	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
136	133, 135	cnf2dd 39003	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ 𝑧 = 𝐸)))
137	126, 136	cnfn1dd 39004	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ 𝑧 = 𝐸))
138		tsan3 39055	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐹 ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
139	138	a1d 26	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐹 ∨ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
140	103, 139	cnfn2dd 39005	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → 𝑧 = 𝐹))
141		tsbi3 39047	. . . . . . . . . . . . . . . . 17 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
142	141	a1d 26	. . . . . . . . . . . . . . . 16 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
143	142	or32dd 39006	. . . . . . . . . . . . . . 15 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ((𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ ¬ 𝑧 = 𝐹)))
144	140, 143	cnfn2dd 39005	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → (𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
145	137, 144	cnf1dd 39002	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹) → ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
146	125, 145	contrd 39009	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))
147	146	a1d 26	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
148	127	a1d 26	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))))
149	95, 148	cnf2dd 39003	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
150	64	a1d 26	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) ∨ (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))))
151	149, 150	cnf2dd 39003	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
152	147, 151	cnf2dd 39003	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
153	61	a1d 26	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
154	152, 153	cnfn2dd 39005	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
155		tsan3 39055	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑦 ∈ 𝐶 ∨ ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶)))
156	155	a1d 26	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑦 ∈ 𝐶 ∨ ¬ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶))))
157	154, 156	cnfn2dd 39005	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦 ∈ 𝐶))
158		tsan3 39055	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (𝑧 = 𝐸 ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)))
159	158	a1d 26	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑧 = 𝐸 ∨ ¬ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸))))
160	152, 159	cnfn2dd 39005	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑧 = 𝐸))
161	94, 81	sylibd 242	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑥 ∈ 𝐵))
162	157, 116	sylibd 242	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → 𝑦 ∈ 𝐷))
163	161, 162	jcad 522	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷)))
164		tsan1 39053	. . . . . . . . . . . . . 14 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
165	164	a1d 26	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ 𝑧 = 𝐹) ∨ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))))
166	147, 165	cnf2dd 39003	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∨ ¬ 𝑧 = 𝐹)))
167	163, 166	cnfn1dd 39004	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ 𝑧 = 𝐹))
168		tsbi4 39048	. . . . . . . . . . . . 13 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
169	168	a1d 26	. . . . . . . . . . . 12 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ 𝑧 = 𝐹) ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
170	169	or32dd 39006	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ 𝑧 = 𝐹)))
171	167, 170	cnf2dd 39003	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑧 = 𝐸 ∨ ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
172	160, 171	cnfn1dd 39004	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))
173		tsim1 39042	. . . . . . . . . . 11 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ((¬ 𝑦 ∈ 𝐶 ∨ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
174	173	a1d 26	. . . . . . . . . 10 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦 ∈ 𝐶 ∨ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)) ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
175	174	or32dd 39006	. . . . . . . . 9 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ((¬ 𝑦 ∈ 𝐶 ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))) ∨ (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
176	172, 175	cnf2dd 39003	. . . . . . . 8 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → (¬ 𝑦 ∈ 𝐶 ∨ ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))))
177	157, 176	cnfn1dd 39004	. . . . . . 7 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → (¬ ⊥ → ¬ (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹))))
178	101, 177	contrd 39009	. . . . . 6 ⊢ (¬ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹))) → ⊥)
179	178	efald2 38992	. . . . 5 ⊢ ((((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
180	179	alimi 1844	. . . 4 ⊢ (∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
181	180	2alimi 1845	. . 3 ⊢ (∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵) ∧ (𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷)) ∧ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐶 → (𝑧 = 𝐸 ↔ 𝑧 = 𝐹)))) → ∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)))
182		oprabbi 39073	. . 3 ⊢ (∀𝑥∀𝑦∀𝑧(((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸) ↔ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)})
183	58, 181, 182	3syl 19	. 2 ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)} = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)})
184		df-mpo 7423	. 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐶) ∧ 𝑧 = 𝐸)}
185		df-mpo 7423	. 2 ⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹) = {⟨⟨𝑥, 𝑦⟩, 𝑧⟩ ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐷) ∧ 𝑧 = 𝐹)}
186	183, 184, 185	3eqtr4g 2821	1 ⊢ (((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐶 𝐸 = 𝐹) → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐶 ↦ 𝐸) = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐷 ↦ 𝐹))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861  ∀wal 1568   = wceq 1570  ⊥wfal 1582   ∈ wcel 2145  Ⅎwnfc 2908  ∀wral 3077  {coprab 7419   ∈ cmpo 7420

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-13 2402  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ral 3078  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-oprab 7422  df-mpo 7423

This theorem is used by: (None)