Theorem xpfin ≪ | index | src | ≫

theorem xpfin (A B: set): $ finite A -> finite B -> finite (Xp A B) $;

Step	Hyp	Ref	Expression
1		lteq2	z = m + n, 0 -> (p < z <-> p < m + n, 0)
2	1	imeq2d	z = m + n, 0 -> (p e. Xp A B -> p < z <-> p e. Xp A B -> p < m + n, 0)
3	2	aleqd	z = m + n, 0 -> (A. p (p e. Xp A B -> p < z) <-> A. p (p e. Xp A B -> p < m + n, 0))
4	3	iexe	A. p (p e. Xp A B -> p < m + n, 0) -> E. z A. p (p e. Xp A B -> p < z)
5	4	conv finite	A. p (p e. Xp A B -> p < m + n, 0) -> finite (Xp A B)
6		elxp	p e. Xp A B <-> fst p e. A /\ snd p e. B
7		lteq1	fst p, snd p = p -> (fst p, snd p < m + n, 0 <-> p < m + n, 0)
8		fstsnd	fst p, snd p = p
9	7, 8	ax_mp	fst p, snd p < m + n, 0 <-> p < m + n, 0
10		ltnle	snd p < n <-> ~n <= snd p
11		ltnle	fst p, snd p < m + n, 0 <-> ~m + n, 0 <= fst p, snd p
12	10, 11	imeqi	snd p < n -> fst p, snd p < m + n, 0 <-> ~n <= snd p -> ~m + n, 0 <= fst p, snd p
13		prlem2	m + n, 0 <= fst p, snd p -> m + n + 0 <= fst p + snd p
14		leeq1	m + n + 0 = m + n -> (m + n + 0 <= fst p + snd p <-> m + n <= fst p + snd p)
15		add0	m + n + 0 = m + n
16	14, 15	ax_mp	m + n + 0 <= fst p + snd p <-> m + n <= fst p + snd p
17		leadd2	n <= snd p <-> fst p + n <= fst p + snd p
18		letr	fst p + n <= m + n -> m + n <= fst p + snd p -> fst p + n <= fst p + snd p
19		leadd1	fst p <= m <-> fst p + n <= m + n
20		ltle	fst p < m -> fst p <= m
21	19, 20	sylib	fst p < m -> fst p + n <= m + n
22	18, 21	syl	fst p < m -> m + n <= fst p + snd p -> fst p + n <= fst p + snd p
23	17, 22	syl6ibr	fst p < m -> m + n <= fst p + snd p -> n <= snd p
24	16, 23	syl5bi	fst p < m -> m + n + 0 <= fst p + snd p -> n <= snd p
25	13, 24	syl5	fst p < m -> m + n, 0 <= fst p, snd p -> n <= snd p
26	25	con3d	fst p < m -> ~n <= snd p -> ~m + n, 0 <= fst p, snd p
27	12, 26	sylibr	fst p < m -> snd p < n -> fst p, snd p < m + n, 0
28	27	imp	fst p < m /\ snd p < n -> fst p, snd p < m + n, 0
29	9, 28	sylib	fst p < m /\ snd p < n -> p < m + n, 0
30		eleq1	x = fst p -> (x e. A <-> fst p e. A)
31		lteq1	x = fst p -> (x < m <-> fst p < m)
32	30, 31	imeqd	x = fst p -> (x e. A -> x < m <-> fst p e. A -> fst p < m)
33	32	eale	A. x (x e. A -> x < m) -> fst p e. A -> fst p < m
34	33	anwl	A. x (x e. A -> x < m) /\ A. y (y e. B -> y < n) -> fst p e. A -> fst p < m
35		eleq1	y = snd p -> (y e. B <-> snd p e. B)
36		lteq1	y = snd p -> (y < n <-> snd p < n)
37	35, 36	imeqd	y = snd p -> (y e. B -> y < n <-> snd p e. B -> snd p < n)
38	37	eale	A. y (y e. B -> y < n) -> snd p e. B -> snd p < n
39	38	anwr	A. x (x e. A -> x < m) /\ A. y (y e. B -> y < n) -> snd p e. B -> snd p < n
40	34, 39	animd	A. x (x e. A -> x < m) /\ A. y (y e. B -> y < n) -> fst p e. A /\ snd p e. B -> fst p < m /\ snd p < n
41	29, 40	syl6	A. x (x e. A -> x < m) /\ A. y (y e. B -> y < n) -> fst p e. A /\ snd p e. B -> p < m + n, 0
42	6, 41	syl5bi	A. x (x e. A -> x < m) /\ A. y (y e. B -> y < n) -> p e. Xp A B -> p < m + n, 0
43	42	iald	A. x (x e. A -> x < m) /\ A. y (y e. B -> y < n) -> A. p (p e. Xp A B -> p < m + n, 0)
44	5, 43	syl	A. x (x e. A -> x < m) /\ A. y (y e. B -> y < n) -> finite (Xp A B)
45	44	eexda	A. x (x e. A -> x < m) -> E. n A. y (y e. B -> y < n) -> finite (Xp A B)
46	45	conv finite	A. x (x e. A -> x < m) -> finite B -> finite (Xp A B)
47	46	eex	E. m A. x (x e. A -> x < m) -> finite B -> finite (Xp A B)
48	47	conv finite	finite A -> finite B -> finite (Xp A B)

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)