Theorem axtcond 36666

Description: A version of the Axiom of Transitive Containment with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2377. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)

Assertion

Ref	Expression
axtcond	⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))

Proof of Theorem axtcond

Dummy variables 𝑢 𝑡 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axtco2 36662	. . . 4 ⊢ ∃𝑤∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))
2		nfnae 2439	. . . . . 6 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑦
3		nfnae 2439	. . . . . 6 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑧
4		nfnae 2439	. . . . . 6 ⊢ Ⅎ𝑦 ¬ ∀𝑦 𝑦 = 𝑧
5	2, 3, 4	nf3an 1903	. . . . 5 ⊢ Ⅎ𝑦(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧)
6		nfv 1916	. . . . . . . 8 ⊢ Ⅎ𝑦∀𝑣((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤))
7		equequ2 2028	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑥 → (𝑣 = 𝑡 ↔ 𝑣 = 𝑥))
8	7	orbi1d 917	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → ((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) ↔ (𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤)))
9		elequ1 2121	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ 𝑣 ↔ 𝑥 ∈ 𝑣))
10		elequ1 2121	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤))
11	9, 10	imbi12d 344	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤) ↔ (𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
12	11	cbvalvw 2038	. . . . . . . . . . 11 ⊢ (∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤) ↔ ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))
13	12	a1i 11	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → (∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤) ↔ ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
14	8, 13	imbi12d 344	. . . . . . . . 9 ⊢ (𝑡 = 𝑥 → (((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤)) ↔ ((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))))
15	14	albidv 1922	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (∀𝑣((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤)) ↔ ∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))))
16	6, 15	dvelimnf 2458	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
17	16	naecoms 2434	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
18	17	3ad2ant1 1134	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
19		nfnae 2439	. . . . . . . . 9 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
20		nfnae 2439	. . . . . . . . 9 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑧
21		nfnae 2439	. . . . . . . . 9 ⊢ Ⅎ𝑧 ¬ ∀𝑦 𝑦 = 𝑧
22	19, 20, 21	nf3an 1903	. . . . . . . 8 ⊢ Ⅎ𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧)
23		nfeqf2 2382	. . . . . . . . . 10 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑤 = 𝑦)
24	23	naecoms 2434	. . . . . . . . 9 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 = 𝑦)
25	24	3ad2ant3 1136	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑦)
26	22, 25	nfan1 2208	. . . . . . 7 ⊢ Ⅎ𝑧((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦)
27		simpl2 1194	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑧)
28		nfv 1916	. . . . . . . . . 10 ⊢ Ⅎ𝑧((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤))
29	28, 14	dvelimnf 2458	. . . . . . . . 9 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
30	29	naecoms 2434	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
31	27, 30	syl 17	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → Ⅎ𝑧((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
32		equequ1 2027	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 = 𝑥 ↔ 𝑧 = 𝑥))
33	32	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑣 = 𝑥 ↔ 𝑧 = 𝑥))
34		elequ12 2132	. . . . . . . . . . . . 13 ⊢ ((𝑣 = 𝑧 ∧ 𝑤 = 𝑦) → (𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦))
35	34	ancoms 458	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦))
36	33, 35	orbi12d 919	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → ((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) ↔ (𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦)))
37	36	adantl 481	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → ((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) ↔ (𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦)))
38		nfnae 2439	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
39		nfnae 2439	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑧
40	38, 39	nfan 1901	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
41		nfeqf2 2382	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 = 𝑦)
42	41	adantr 480	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤 = 𝑦)
43		nfeqf2 2382	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑣 = 𝑧)
44	43	adantl 481	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑣 = 𝑧)
45	42, 44	nfand 1899	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑤 = 𝑦 ∧ 𝑣 = 𝑧))
46	40, 45	nfan1 2208	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧))
47		elequ2 2129	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑧 → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑧))
48	47	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑧))
49		elequ2 2129	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦))
50	49	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦))
51	48, 50	imbi12d 344	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → ((𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤) ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
52	51	adantl 481	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → ((𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤) ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
53	46, 52	albid 2230	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → (∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤) ↔ ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
54	37, 53	imbi12d 344	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → (((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
55	54	expr 456	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑣 = 𝑧 → (((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
56	55	3adantl3 1170	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑣 = 𝑧 → (((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
57	26, 31, 56	cbvaldw 2343	. . . . . 6 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
58	57	ex 412	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑤 = 𝑦 → (∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
59	5, 18, 58	cbvexdw 2344	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∃𝑤∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
60	1, 59	mpbii 233	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
61	60	3exp 1120	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
62		nfae 2438	. . . . . 6 ⊢ Ⅎ𝑧∀𝑦 𝑦 = 𝑧
63		nfae 2438	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑦 𝑦 = 𝑧
64		elequ2 2129	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))
65	64	sps 2193	. . . . . . . . 9 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))
66	65	biimprd 248	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
67	63, 66	alrimi 2221	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
68	67	a1d 25	. . . . . 6 ⊢ (∀𝑦 𝑦 = 𝑧 → ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
69	62, 68	alrimi 2221	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑧 → ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
70	69	19.8ad 2190	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
71	70	a1i 11	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
72		ax-nul 5241	. . . . 5 ⊢ ∃𝑦∀𝑢 ¬ 𝑢 ∈ 𝑦
73		nfv 1916	. . . . . . . . 9 ⊢ Ⅎ𝑧∀𝑢 ¬ 𝑢 ∈ 𝑡
74		elequ2 2129	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑦))
75	74	notbid 318	. . . . . . . . . 10 ⊢ (𝑡 = 𝑦 → (¬ 𝑢 ∈ 𝑡 ↔ ¬ 𝑢 ∈ 𝑦))
76	75	albidv 1922	. . . . . . . . 9 ⊢ (𝑡 = 𝑦 → (∀𝑢 ¬ 𝑢 ∈ 𝑡 ↔ ∀𝑢 ¬ 𝑢 ∈ 𝑦))
77	73, 76	dvelimnf 2458	. . . . . . . 8 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧∀𝑢 ¬ 𝑢 ∈ 𝑦)
78	77	naecoms 2434	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∀𝑢 ¬ 𝑢 ∈ 𝑦)
79		elequ2 2129	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝑢 ∈ 𝑧 ↔ 𝑢 ∈ 𝑦))
80	79	notbid 318	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → (¬ 𝑢 ∈ 𝑧 ↔ ¬ 𝑢 ∈ 𝑦))
81	80	albidv 1922	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 ↔ ∀𝑢 ¬ 𝑢 ∈ 𝑦))
82	81	biimprcd 250	. . . . . . . . . 10 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → (𝑧 = 𝑦 → ∀𝑢 ¬ 𝑢 ∈ 𝑧))
83		elirrv 9503	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑥 ∈ 𝑥
84		elequ2 2129	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑥 ↔ 𝑥 ∈ 𝑧))
85	83, 84	mtbii 326	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → ¬ 𝑥 ∈ 𝑧)
86	85	pm2.21d 121	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
87	86	alimi 1813	. . . . . . . . . . . 12 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
88	87	a1d 25	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
89		nfv 1916	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑢 ¬ 𝑢 ∈ 𝑡
90		elequ2 2129	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑧 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑧))
91	90	notbid 318	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → (¬ 𝑢 ∈ 𝑡 ↔ ¬ 𝑢 ∈ 𝑧))
92	91	albidv 1922	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑡 ↔ ∀𝑢 ¬ 𝑢 ∈ 𝑧))
93	89, 92	dvelimnf 2458	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥∀𝑢 ¬ 𝑢 ∈ 𝑧)
94		elequ1 2121	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
95	94	notbid 318	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → (¬ 𝑢 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑧))
96	95	spvv 1990	. . . . . . . . . . . . . 14 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧)
97	96	pm2.21d 121	. . . . . . . . . . . . 13 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
98	97	a1i 11	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
99	39, 93, 98	alrimdd 2222	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
100	88, 99	pm2.61i 182	. . . . . . . . . 10 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
101	82, 100	syl6 35	. . . . . . . . 9 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → (𝑧 = 𝑦 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
102		elequ1 2121	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
103	102	notbid 318	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → (¬ 𝑢 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦))
104	103	spvv 1990	. . . . . . . . . 10 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑦)
105	104	pm2.21d 121	. . . . . . . . 9 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
106	101, 105	jaod 860	. . . . . . . 8 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
107	106	a1i 11	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
108	21, 78, 107	alrimdd 2222	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
109	4, 108	eximd 2224	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑦∀𝑢 ¬ 𝑢 ∈ 𝑦 → ∃𝑦∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
110	72, 109	mpi 20	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
111		nfae 2438	. . . . 5 ⊢ Ⅎ𝑦∀𝑥 𝑥 = 𝑦
112		nfae 2438	. . . . . 6 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
113		equequ2 2028	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
114	113	sps 2193	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
115	114	orbi1d 917	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑦 → ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) ↔ (𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦)))
116	115	imbi1d 341	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑦 → (((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
117	112, 116	albid 2230	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
118	111, 117	exbid 2231	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ∃𝑦∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
119	110, 118	imbitrrid 246	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
120	71, 119	pm2.61d 179	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
121		nfae 2438	. . . 4 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑧
122	87	a1d 25	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
123	121, 122	alrimi 2221	. . 3 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
124	123	19.8ad 2190	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
125	61, 120, 124, 70	pm2.61iii 185	1 ⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087  ∀wal 1540  ∃wex 1781  Ⅎwnf 1785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-13 2377  ax-sep 5231  ax-nul 5241  ax-pr 5368  ax-reg 9498  ax-tco 36660

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-nf 1786

This theorem is referenced by: (None)