axinfndlem1

Description: Lemma for the Axiom of Infinity with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 5-Jan-2002)

		Ref	Expression
	Assertion	axinfndlem1	$⊢ \forall x y \in z \to \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))$

Proof

Step	Hyp	Ref	Expression
1		zfinf	$⊢ \exists w (y \in w \land \forall y (y \in w \to \exists z (y \in z \land z \in w)))$
2		nfnae	$⊢ Ⅎ x \neg \forall x x = y$
3		nfnae	$⊢ Ⅎ x \neg \forall x x = z$
4	2 3	nfan	$⊢ Ⅎ x (\neg \forall x x = y \land \neg \forall x x = z)$
5		nfcvf	$⊢ \neg \forall x x = y \to \underline{Ⅎ} x y$
6	5	adantr	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to \underline{Ⅎ} x y$
7		nfcvd	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to \underline{Ⅎ} x w$
8	6 7	nfeld	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ x y \in w$
9		nfnae	$⊢ Ⅎ y \neg \forall x x = y$
10		nfnae	$⊢ Ⅎ y \neg \forall x x = z$
11	9 10	nfan	$⊢ Ⅎ y (\neg \forall x x = y \land \neg \forall x x = z)$
12		nfnae	$⊢ Ⅎ z \neg \forall x x = y$
13		nfnae	$⊢ Ⅎ z \neg \forall x x = z$
14	12 13	nfan	$⊢ Ⅎ z (\neg \forall x x = y \land \neg \forall x x = z)$
15		nfcvf	$⊢ \neg \forall x x = z \to \underline{Ⅎ} x z$
16	15	adantl	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to \underline{Ⅎ} x z$
17	6 16	nfeld	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ x y \in z$
18	16 7	nfeld	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ x z \in w$
19	17 18	nfand	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ x (y \in z \land z \in w)$
20	14 19	nfexd	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ x \exists z (y \in z \land z \in w)$
21	8 20	nfimd	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ x (y \in w \to \exists z (y \in z \land z \in w))$
22	11 21	nfald	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ x \forall y (y \in w \to \exists z (y \in z \land z \in w))$
23	8 22	nfand	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ x (y \in w \land \forall y (y \in w \to \exists z (y \in z \land z \in w)))$
24		simpr	$⊢ ((\neg \forall x x = y \land \neg \forall x x = z) \land w = x) \to w = x$
25	24	eleq2d	$⊢ ((\neg \forall x x = y \land \neg \forall x x = z) \land w = x) \to (y \in w \leftrightarrow y \in x)$
26		nfcvd	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to \underline{Ⅎ} y w$
27		nfcvf2	$⊢ \neg \forall x x = y \to \underline{Ⅎ} y x$
28	27	adantr	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to \underline{Ⅎ} y x$
29	26 28	nfeqd	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ y w = x$
30	11 29	nfan1	$⊢ Ⅎ y ((\neg \forall x x = y \land \neg \forall x x = z) \land w = x)$
31		nfcvd	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to \underline{Ⅎ} z w$
32		nfcvf2	$⊢ \neg \forall x x = z \to \underline{Ⅎ} z x$
33	32	adantl	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to \underline{Ⅎ} z x$
34	31 33	nfeqd	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to Ⅎ z w = x$
35	14 34	nfan1	$⊢ Ⅎ z ((\neg \forall x x = y \land \neg \forall x x = z) \land w = x)$
36		elequ2	$⊢ w = x \to (z \in w \leftrightarrow z \in x)$
37	36	anbi2d	$⊢ w = x \to ((y \in z \land z \in w) \leftrightarrow (y \in z \land z \in x))$
38	37	adantl	$⊢ ((\neg \forall x x = y \land \neg \forall x x = z) \land w = x) \to ((y \in z \land z \in w) \leftrightarrow (y \in z \land z \in x))$
39	35 38	exbid	$⊢ ((\neg \forall x x = y \land \neg \forall x x = z) \land w = x) \to (\exists z (y \in z \land z \in w) \leftrightarrow \exists z (y \in z \land z \in x))$
40	25 39	imbi12d	$⊢ ((\neg \forall x x = y \land \neg \forall x x = z) \land w = x) \to ((y \in w \to \exists z (y \in z \land z \in w)) \leftrightarrow (y \in x \to \exists z (y \in z \land z \in x)))$
41	30 40	albid	$⊢ ((\neg \forall x x = y \land \neg \forall x x = z) \land w = x) \to (\forall y (y \in w \to \exists z (y \in z \land z \in w)) \leftrightarrow \forall y (y \in x \to \exists z (y \in z \land z \in x)))$
42	25 41	anbi12d	$⊢ ((\neg \forall x x = y \land \neg \forall x x = z) \land w = x) \to ((y \in w \land \forall y (y \in w \to \exists z (y \in z \land z \in w))) \leftrightarrow (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x))))$
43	42	ex	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to (w = x \to ((y \in w \land \forall y (y \in w \to \exists z (y \in z \land z \in w))) \leftrightarrow (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))))$
44	4 23 43	cbvexd	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to (\exists w (y \in w \land \forall y (y \in w \to \exists z (y \in z \land z \in w))) \leftrightarrow \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x))))$
45	1 44	mpbii	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))$
46	45	a1d	$⊢ (\neg \forall x x = y \land \neg \forall x x = z) \to (\forall x y \in z \to \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x))))$
47	46	ex	$⊢ \neg \forall x x = y \to (\neg \forall x x = z \to (\forall x y \in z \to \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))))$
48		nd1	$⊢ \forall x x = y \to \neg \forall x y \in z$
49	48	pm2.21d	$⊢ \forall x x = y \to (\forall x y \in z \to \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x))))$
50		nd2	$⊢ \forall x x = z \to \neg \forall x y \in z$
51	50	pm2.21d	$⊢ \forall x x = z \to (\forall x y \in z \to \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x))))$
52	47 49 51	pm2.61ii	$⊢ \forall x y \in z \to \exists x (y \in x \land \forall y (y \in x \to \exists z (y \in z \land z \in x)))$

Metamath Proof Explorer

Theorem axinfndlem1

Proof