Theorem zfcndinf 4893

Description: Axiom of Infinity, reproved from conditionless ZFC axioms. Since we have already reproved Extensionality, Replacement, and Power Sets, we are justified in referencing theorem el 2719 in the proof.

Assertion

Ref	Expression
zfcndinf	|- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))

Distinct variable group:   x,y,z,w

Proof of Theorem zfcndinf

Step	Hyp	Ref	Expression
1		el 2719	. . 3 |- E.w x e. w
2		ax-17 1190	. . . . . 6 |- (x e. y -> A.w x e. y)
3		hbe1 990	. . . . . . . 8 |- (E.w(x e. w /\ w e. y) -> A.wE.w(x e. w /\ w e. y))
4	2, 3	hbim 983	. . . . . . 7 |- ((x e. y -> E.w(x e. w /\ w e. y)) -> A.w(x e. y -> E.w(x e. w /\ w e. y)))
5	4	hbal 981	. . . . . 6 |- (A.x(x e. y -> E.w(x e. w /\ w e. y)) -> A.wA.x(x e. y -> E.w(x e. w /\ w e. y)))
6	2, 5	hban 985	. . . . 5 |- ((x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))) -> A.w(x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))))
7	6	hbex 982	. . . 4 |- (E.y(x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))) -> A.wE.y(x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))))
8		ax-17 1190	. . . . 5 |- (x e. w -> A.y x e. w)
9		axinfnd 4881	. . . . . 6 |- E.y(x e. w -> (x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))))
10	9	19.35i 1052	. . . . 5 |- (A.y x e. w -> E.y(x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))))
11	8, 10	syl 10	. . . 4 |- (x e. w -> E.y(x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))))
12	7, 11	19.23ai 1040	. . 3 |- (E.w x e. w -> E.y(x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))))
13	1, 12	ax-mp 7	. 2 |- E.y(x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y)))
14		elequ1 1123	. . . . . 6 |- (z = x -> (z e. y <-> x e. y))
15		elequ1 1123	. . . . . . . 8 |- (z = x -> (z e. w <-> x e. w))
16	15	anbi1d 615	. . . . . . 7 |- (z = x -> ((z e. w /\ w e. y) <-> (x e. w /\ w e. y)))
17	16	exbidv 1261	. . . . . 6 |- (z = x -> (E.w(z e. w /\ w e. y) <-> E.w(x e. w /\ w e. y)))
18	14, 17	imbi12d 624	. . . . 5 |- (z = x -> ((z e. y -> E.w(z e. w /\ w e. y)) <-> (x e. y -> E.w(x e. w /\ w e. y))))
19	18	cbvalv 1296	. . . 4 |- (A.z(z e. y -> E.w(z e. w /\ w e. y)) <-> A.x(x e. y -> E.w(x e. w /\ w e. y)))
20	19	anbi2i 479	. . 3 |- ((x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y))) <-> (x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))))
21	20	exbii 1027	. 2 |- (E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y))) <-> E.y(x e. y /\ A.x(x e. y -> E.w(x e. w /\ w e. y))))
22	13, 21	mpbir 190	1 |- E.y(x e. y /\ A.z(z e. y -> E.w(z e. w /\ w e. y)))

Syntax hints:   -> wi 3   /\ wa 223  A.wal 950  E.wex 956   = wceq 1099   e. wcel 1105

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-7 954  ax-gen 955  ax-8 1101  ax-9 1102  ax-10 1103  ax-12 1104  ax-13 1107  ax-14 1108  ax-11 1180  ax-17 1190  ax-16 1194  ax-11o 1202  ax-ext 1436  ax-sep 2671  ax-pow 2710  ax-reg 4517  ax-inf 4546

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 957  df-sb 1155  df-eu 1359  df-mo 1360  df-clab 1441  df-cleq 1446  df-clel 1449  df-ne 1563  df-ral 1625  df-rex 1626  df-v 1787  df-dif 2020  df-un 2021  df-in 2022  df-ss 2024  df-nul 2252  df-pw 2373  df-sn 2383  df-pr 2384

Copyright terms: Public domain