fin1a2lem9

Description: Lemma for fin1a2 . In a chain of finite sets, initial segments are finite. (Contributed by Stefan O'Rear, 8-Nov-2014)

		Ref	Expression
	Assertion	fin1a2lem9	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to \{b \in X \| b ≼ A\} \in Fin$

Proof

Step	Hyp	Ref	Expression
1		onfin2	$⊢ ω = On \cap Fin$
2		inss2	$⊢ On \cap Fin \subseteq Fin$
3	1 2	eqsstri	$⊢ ω \subseteq Fin$
4		peano2	$⊢ A \in ω \to suc A \in ω$
5	3 4	sselid	$⊢ A \in ω \to suc A \in Fin$
6	5	3ad2ant3	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to suc A \in Fin$
7	4	3ad2ant3	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to suc A \in ω$
8		breq1	$⊢ b = c \to (b ≼ A \leftrightarrow c ≼ A)$
9	8	elrab	$⊢ c \in \{b \in X \| b ≼ A\} \leftrightarrow (c \in X \land c ≼ A)$
10		simprr	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to c ≼ A$
11		simpl2	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to X \subseteq Fin$
12		simprl	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to c \in X$
13	11 12	sseldd	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to c \in Fin$
14		finnum	$⊢ c \in Fin \to c \in dom card$
15	13 14	syl	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to c \in dom card$
16		simpl3	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to A \in ω$
17	3 16	sselid	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to A \in Fin$
18		finnum	$⊢ A \in Fin \to A \in dom card$
19	17 18	syl	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to A \in dom card$
20		carddom2	$⊢ (c \in dom card \land A \in dom card) \to (card (c) \subseteq card (A) \leftrightarrow c ≼ A)$
21	15 19 20	syl2anc	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to (card (c) \subseteq card (A) \leftrightarrow c ≼ A)$
22	10 21	mpbird	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land c ≼ A)) \to card (c) \subseteq card (A)$
23	22	ex	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to ((c \in X \land c ≼ A) \to card (c) \subseteq card (A))$
24		cardnn	$⊢ A \in ω \to card (A) = A$
25	24	sseq2d	$⊢ A \in ω \to (card (c) \subseteq card (A) \leftrightarrow card (c) \subseteq A)$
26		cardon	$⊢ card (c) \in On$
27		nnon	$⊢ A \in ω \to A \in On$
28		onsssuc	$⊢ (card (c) \in On \land A \in On) \to (card (c) \subseteq A \leftrightarrow card (c) \in suc A)$
29	26 27 28	sylancr	$⊢ A \in ω \to (card (c) \subseteq A \leftrightarrow card (c) \in suc A)$
30	25 29	bitrd	$⊢ A \in ω \to (card (c) \subseteq card (A) \leftrightarrow card (c) \in suc A)$
31	30	3ad2ant3	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to (card (c) \subseteq card (A) \leftrightarrow card (c) \in suc A)$
32	23 31	sylibd	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to ((c \in X \land c ≼ A) \to card (c) \in suc A)$
33	9 32	biimtrid	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to (c \in \{b \in X \| b ≼ A\} \to card (c) \in suc A)$
34		elrabi	$⊢ c \in \{b \in X \| b ≼ A\} \to c \in X$
35		elrabi	$⊢ d \in \{b \in X \| b ≼ A\} \to d \in X$
36		ssel	$⊢ X \subseteq Fin \to (c \in X \to c \in Fin)$
37		ssel	$⊢ X \subseteq Fin \to (d \in X \to d \in Fin)$
38	36 37	anim12d	$⊢ X \subseteq Fin \to ((c \in X \land d \in X) \to (c \in Fin \land d \in Fin))$
39	38	imp	$⊢ (X \subseteq Fin \land (c \in X \land d \in X)) \to (c \in Fin \land d \in Fin)$
40	39	3ad2antl2	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land d \in X)) \to (c \in Fin \land d \in Fin)$
41		sorpssi	$⊢ ([\subset] Or X \land (c \in X \land d \in X)) \to (c \subseteq d \lor d \subseteq c)$
42	41	3ad2antl1	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land d \in X)) \to (c \subseteq d \lor d \subseteq c)$
43		finnum	$⊢ d \in Fin \to d \in dom card$
44		carden2	$⊢ (c \in dom card \land d \in dom card) \to (card (c) = card (d) \leftrightarrow c \approx d)$
45	14 43 44	syl2an	$⊢ (c \in Fin \land d \in Fin) \to (card (c) = card (d) \leftrightarrow c \approx d)$
46	45	adantr	$⊢ ((c \in Fin \land d \in Fin) \land (c \subseteq d \lor d \subseteq c)) \to (card (c) = card (d) \leftrightarrow c \approx d)$
47		fin23lem25	$⊢ (c \in Fin \land d \in Fin \land (c \subseteq d \lor d \subseteq c)) \to (c \approx d \leftrightarrow c = d)$
48	47	3expa	$⊢ ((c \in Fin \land d \in Fin) \land (c \subseteq d \lor d \subseteq c)) \to (c \approx d \leftrightarrow c = d)$
49	48	biimpd	$⊢ ((c \in Fin \land d \in Fin) \land (c \subseteq d \lor d \subseteq c)) \to (c \approx d \to c = d)$
50	46 49	sylbid	$⊢ ((c \in Fin \land d \in Fin) \land (c \subseteq d \lor d \subseteq c)) \to (card (c) = card (d) \to c = d)$
51	40 42 50	syl2anc	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land d \in X)) \to (card (c) = card (d) \to c = d)$
52		fveq2	$⊢ c = d \to card (c) = card (d)$
53	51 52	impbid1	$⊢ (([\subset] Or X \land X \subseteq Fin \land A \in ω) \land (c \in X \land d \in X)) \to (card (c) = card (d) \leftrightarrow c = d)$
54	53	ex	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to ((c \in X \land d \in X) \to (card (c) = card (d) \leftrightarrow c = d))$
55	34 35 54	syl2ani	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to ((c \in \{b \in X \| b ≼ A\} \land d \in \{b \in X \| b ≼ A\}) \to (card (c) = card (d) \leftrightarrow c = d))$
56	33 55	dom2d	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to (suc A \in ω \to \{b \in X \| b ≼ A\} ≼ suc A)$
57	7 56	mpd	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to \{b \in X \| b ≼ A\} ≼ suc A$
58		domfi	$⊢ (suc A \in Fin \land \{b \in X \| b ≼ A\} ≼ suc A) \to \{b \in X \| b ≼ A\} \in Fin$
59	6 57 58	syl2anc	$⊢ ([\subset] Or X \land X \subseteq Fin \land A \in ω) \to \{b \in X \| b ≼ A\} \in Fin$

Metamath Proof Explorer

Theorem fin1a2lem9

Proof