Theorem expset ≪ | index | src | ≫

theorem expset (A: set) {a: nat}: $ finite A <-> E. a pset a == A $;

Step	Hyp	Ref	Expression
1		psetsep	E. a pset a == {y \| y < n /\ y e. A}
2		bian1a	(y e. A -> y < n) -> (y < n /\ y e. A <-> y e. A)
3		eleq1	x = y -> (x e. A <-> y e. A)
4		lteq1	x = y -> (x < n <-> y < n)
5	3, 4	imeqd	x = y -> (x e. A -> x < n <-> y e. A -> y < n)
6	5	eale	A. x (x e. A -> x < n) -> y e. A -> y < n
7	2, 6	syl	A. x (x e. A -> x < n) -> (y < n /\ y e. A <-> y e. A)
8	7	eqab1d	A. x (x e. A -> x < n) -> {y \| y < n /\ y e. A} == A
9	8	eqseq2d	A. x (x e. A -> x < n) -> (pset a == {y \| y < n /\ y e. A} <-> pset a == A)
10	9	exeqd	A. x (x e. A -> x < n) -> (E. a pset a == {y \| y < n /\ y e. A} <-> E. a pset a == A)
11	1, 10	mpbii	A. x (x e. A -> x < n) -> E. a pset a == A
12	11	eex	E. n A. x (x e. A -> x < n) -> E. a pset a == A
13		lesucid	fst a * suc x <= suc (fst a * suc x)
14		letr	suc x <= fst a * suc x -> fst a * suc x <= suc (fst a * suc x) -> suc x <= suc (fst a * suc x)
15	13, 14	mpi	suc x <= fst a * suc x -> suc x <= suc (fst a * suc x)
16		leeq1	1 * suc x = suc x -> (1 * suc x <= fst a * suc x <-> suc x <= fst a * suc x)
17		mul11	1 * suc x = suc x
18	16, 17	ax_mp	1 * suc x <= fst a * suc x <-> suc x <= fst a * suc x
19		lemul1a	1 <= fst a -> 1 * suc x <= fst a * suc x
20		an3l	1 <= fst a /\ 0 < snd a /\ A. y (0 < y /\ y <= x -> y \|\| fst a) /\ suc (fst a * suc x) \|\| snd a -> 1 <= fst a
21		elpset	x e. pset (fst a, snd a) <-> 0 < fst a /\ 0 < snd a /\ A. y (0 < y /\ y <= x -> y \|\| fst a) /\ suc (fst a * suc x) \|\| snd a
22		pseteq	fst a, snd a = a -> pset (fst a, snd a) == pset a
23		fstsnd	fst a, snd a = a
24	22, 23	ax_mp	pset (fst a, snd a) == pset a
25		anll	pset a == A /\ n = snd a /\ x e. A -> pset a == A
26	24, 25	syl5eqs	pset a == A /\ n = snd a /\ x e. A -> pset (fst a, snd a) == A
27	26	eleq2d	pset a == A /\ n = snd a /\ x e. A -> (x e. pset (fst a, snd a) <-> x e. A)
28		anr	pset a == A /\ n = snd a /\ x e. A -> x e. A
29	27, 28	mpbird	pset a == A /\ n = snd a /\ x e. A -> x e. pset (fst a, snd a)
30	21, 29	sylib	pset a == A /\ n = snd a /\ x e. A -> 0 < fst a /\ 0 < snd a /\ A. y (0 < y /\ y <= x -> y \|\| fst a) /\ suc (fst a * suc x) \|\| snd a
31	30	conv d1, lt	pset a == A /\ n = snd a /\ x e. A -> 1 <= fst a /\ 0 < snd a /\ A. y (0 < y /\ y <= x -> y \|\| fst a) /\ suc (fst a * suc x) \|\| snd a
32	20, 31	syl	pset a == A /\ n = snd a /\ x e. A -> 1 <= fst a
33	19, 32	syl	pset a == A /\ n = snd a /\ x e. A -> 1 * suc x <= fst a * suc x
34	18, 33	sylib	pset a == A /\ n = snd a /\ x e. A -> suc x <= fst a * suc x
35	15, 34	syl	pset a == A /\ n = snd a /\ x e. A -> suc x <= suc (fst a * suc x)
36		ltner	0 < snd a -> snd a != 0
37		anllr	0 < fst a /\ 0 < snd a /\ A. y (0 < y /\ y <= x -> y \|\| fst a) /\ suc (fst a * suc x) \|\| snd a -> 0 < snd a
38	37, 30	syl	pset a == A /\ n = snd a /\ x e. A -> 0 < snd a
39	36, 38	syl	pset a == A /\ n = snd a /\ x e. A -> snd a != 0
40	30	anrd	pset a == A /\ n = snd a /\ x e. A -> suc (fst a * suc x) \|\| snd a
41	39, 40	dvdle	pset a == A /\ n = snd a /\ x e. A -> suc (fst a * suc x) <= snd a
42		eqler	n = snd a -> snd a <= n
43		anlr	pset a == A /\ n = snd a /\ x e. A -> n = snd a
44	42, 43	syl	pset a == A /\ n = snd a /\ x e. A -> snd a <= n
45	41, 44	letrd	pset a == A /\ n = snd a /\ x e. A -> suc (fst a * suc x) <= n
46	35, 45	letrd	pset a == A /\ n = snd a /\ x e. A -> suc x <= n
47	46	conv lt	pset a == A /\ n = snd a /\ x e. A -> x < n
48	47	ialda	pset a == A /\ n = snd a -> A. x (x e. A -> x < n)
49	48	iexde	pset a == A -> E. n A. x (x e. A -> x < n)
50	49	eex	E. a pset a == A -> E. n A. x (x e. A -> x < n)
51	12, 50	ibii	E. n A. x (x e. A -> x < n) <-> E. a pset a == A
52	51	conv finite	finite A <-> E. a pset a == A

Axiom use

axs_prop_calc (ax_1, ax_2, ax_3, ax_mp, itru), axs_pred_calc (ax_gen, ax_4, ax_5, ax_6, ax_7, ax_10, ax_11, ax_12), axs_set (elab, ax_8), axs_the (theid, the0), axs_peano (peano1, peano2, peano5, addeq, muleq, add0, addS, mul0, mulS)