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	24	a1i	pset a == A /\ n = snd a /\ x e. A -> pset (fst a, snd a) == pset a
26		anll	pset a == A /\ n = snd a /\ x e. A -> pset a == A
27	25, 26	eqstrd	pset a == A /\ n = snd a /\ x e. A -> pset (fst a, snd a) == A
28	27	eleq2d	pset a == A /\ n = snd a /\ x e. A -> (x e. pset (fst a, snd a) <-> x e. A)
29		anr	pset a == A /\ n = snd a /\ x e. A -> x e. A
30	28, 29	mpbird	pset a == A /\ n = snd a /\ x e. A -> x e. pset (fst a, snd a)
31	21, 30	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
32	31	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
33	20, 32	syl	pset a == A /\ n = snd a /\ x e. A -> 1 <= fst a
34	19, 33	syl	pset a == A /\ n = snd a /\ x e. A -> 1 * suc x <= fst a * suc x
35	18, 34	sylib	pset a == A /\ n = snd a /\ x e. A -> suc x <= fst a * suc x
36	15, 35	syl	pset a == A /\ n = snd a /\ x e. A -> suc x <= suc (fst a * suc x)
37		ltner	0 < snd a -> snd a != 0
38		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
39	38, 31	syl	pset a == A /\ n = snd a /\ x e. A -> 0 < snd a
40	37, 39	syl	pset a == A /\ n = snd a /\ x e. A -> snd a != 0
41	31	anrd	pset a == A /\ n = snd a /\ x e. A -> suc (fst a * suc x) \|\| snd a
42	40, 41	dvdle	pset a == A /\ n = snd a /\ x e. A -> suc (fst a * suc x) <= snd a
43		eqler	n = snd a -> snd a <= n
44		anlr	pset a == A /\ n = snd a /\ x e. A -> n = snd a
45	43, 44	syl	pset a == A /\ n = snd a /\ x e. A -> snd a <= n
46	42, 45	letrd	pset a == A /\ n = snd a /\ x e. A -> suc (fst a * suc x) <= n
47	36, 46	letrd	pset a == A /\ n = snd a /\ x e. A -> suc x <= n
48	47	conv lt	pset a == A /\ n = snd a /\ x e. A -> x < n
49	48	ialda	pset a == A /\ n = snd a -> A. x (x e. A -> x < n)
50	49	iexde	pset a == A -> E. n A. x (x e. A -> x < n)
51	50	eex	E. a pset a == A -> E. n A. x (x e. A -> x < n)
52	12, 51	ibii	E. n A. x (x e. A -> x < n) <-> E. a pset a == A
53	52	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)