fin1a2lem6

Description: Lemma for fin1a2 . Establish that _om can be broken into two equipollent pieces. (Contributed by Stefan O'Rear, 7-Nov-2014)

	Ref	Expression
Hypotheses	fin1a2lem.b	$⊢ E = (x \in ω ⟼ 2_{𝑜} \cdot_{𝑜} x)$
	fin1a2lem.aa	$⊢ S = (x \in On ⟼ suc x)$
Assertion	fin1a2lem6	$⊢ ({S ↾}_{ran E}) : ran E \underset{1-1 onto}{⟶} ω ∖ ran E$

Proof

Step	Hyp	Ref	Expression
1		fin1a2lem.b	$⊢ E = (x \in ω ⟼ 2_{𝑜} \cdot_{𝑜} x)$
2		fin1a2lem.aa	$⊢ S = (x \in On ⟼ suc x)$
3	2	fin1a2lem2	$⊢ S : On \underset{1-1}{⟶} On$
4	1	fin1a2lem4	$⊢ E : ω \underset{1-1}{⟶} ω$
5		f1f	$⊢ E : ω \underset{1-1}{⟶} ω \to E : ω ⟶ ω$
6		frn	$⊢ E : ω ⟶ ω \to ran E \subseteq ω$
7		omsson	$⊢ ω \subseteq On$
8	6 7	sstrdi	$⊢ E : ω ⟶ ω \to ran E \subseteq On$
9	4 5 8	mp2b	$⊢ ran E \subseteq On$
10		f1ores	$⊢ (S : On \underset{1-1}{⟶} On \land ran E \subseteq On) \to ({S ↾}_{ran E}) : ran E \underset{1-1 onto}{⟶} S [ran E]$
11	3 9 10	mp2an	$⊢ ({S ↾}_{ran E}) : ran E \underset{1-1 onto}{⟶} S [ran E]$
12	9	sseli	$⊢ b \in ran E \to b \in On$
13	2	fin1a2lem1	$⊢ b \in On \to S (b) = suc b$
14	12 13	syl	$⊢ b \in ran E \to S (b) = suc b$
15	14	eqeq1d	$⊢ b \in ran E \to (S (b) = a \leftrightarrow suc b = a)$
16	15	rexbiia	$⊢ \exists b \in ran E S (b) = a \leftrightarrow \exists b \in ran E suc b = a$
17	4 5 6	mp2b	$⊢ ran E \subseteq ω$
18	17	sseli	$⊢ b \in ran E \to b \in ω$
19		peano2	$⊢ b \in ω \to suc b \in ω$
20	18 19	syl	$⊢ b \in ran E \to suc b \in ω$
21	1	fin1a2lem5	$⊢ b \in ω \to (b \in ran E \leftrightarrow \neg suc b \in ran E)$
22	21	biimpd	$⊢ b \in ω \to (b \in ran E \to \neg suc b \in ran E)$
23	18 22	mpcom	$⊢ b \in ran E \to \neg suc b \in ran E$
24	20 23	jca	$⊢ b \in ran E \to (suc b \in ω \land \neg suc b \in ran E)$
25		eleq1	$⊢ suc b = a \to (suc b \in ω \leftrightarrow a \in ω)$
26		eleq1	$⊢ suc b = a \to (suc b \in ran E \leftrightarrow a \in ran E)$
27	26	notbid	$⊢ suc b = a \to (\neg suc b \in ran E \leftrightarrow \neg a \in ran E)$
28	25 27	anbi12d	$⊢ suc b = a \to ((suc b \in ω \land \neg suc b \in ran E) \leftrightarrow (a \in ω \land \neg a \in ran E))$
29	24 28	syl5ibcom	$⊢ b \in ran E \to (suc b = a \to (a \in ω \land \neg a \in ran E))$
30	29	rexlimiv	$⊢ \exists b \in ran E suc b = a \to (a \in ω \land \neg a \in ran E)$
31		peano1	$⊢ \emptyset \in ω$
32	1	fin1a2lem3	$⊢ \emptyset \in ω \to E (\emptyset) = 2_{𝑜} \cdot_{𝑜} \emptyset$
33	31 32	ax-mp	$⊢ E (\emptyset) = 2_{𝑜} \cdot_{𝑜} \emptyset$
34		2on	$⊢ 2_{𝑜} \in On$
35		om0	$⊢ 2_{𝑜} \in On \to 2_{𝑜} \cdot_{𝑜} \emptyset = \emptyset$
36	34 35	ax-mp	$⊢ 2_{𝑜} \cdot_{𝑜} \emptyset = \emptyset$
37	33 36	eqtri	$⊢ E (\emptyset) = \emptyset$
38		f1fun	$⊢ E : ω \underset{1-1}{⟶} ω \to Fun E$
39	4 38	ax-mp	$⊢ Fun E$
40		f1dm	$⊢ E : ω \underset{1-1}{⟶} ω \to dom E = ω$
41	4 40	ax-mp	$⊢ dom E = ω$
42	31 41	eleqtrri	$⊢ \emptyset \in dom E$
43		fvelrn	$⊢ (Fun E \land \emptyset \in dom E) \to E (\emptyset) \in ran E$
44	39 42 43	mp2an	$⊢ E (\emptyset) \in ran E$
45	37 44	eqeltrri	$⊢ \emptyset \in ran E$
46		eleq1	$⊢ a = \emptyset \to (a \in ran E \leftrightarrow \emptyset \in ran E)$
47	45 46	mpbiri	$⊢ a = \emptyset \to a \in ran E$
48	47	necon3bi	$⊢ \neg a \in ran E \to a \neq \emptyset$
49		nnsuc	$⊢ (a \in ω \land a \neq \emptyset) \to \exists b \in ω a = suc b$
50	48 49	sylan2	$⊢ (a \in ω \land \neg a \in ran E) \to \exists b \in ω a = suc b$
51		eleq1	$⊢ a = suc b \to (a \in ω \leftrightarrow suc b \in ω)$
52		eleq1	$⊢ a = suc b \to (a \in ran E \leftrightarrow suc b \in ran E)$
53	52	notbid	$⊢ a = suc b \to (\neg a \in ran E \leftrightarrow \neg suc b \in ran E)$
54	51 53	anbi12d	$⊢ a = suc b \to ((a \in ω \land \neg a \in ran E) \leftrightarrow (suc b \in ω \land \neg suc b \in ran E))$
55	54	anbi1d	$⊢ a = suc b \to (((a \in ω \land \neg a \in ran E) \land b \in ω) \leftrightarrow ((suc b \in ω \land \neg suc b \in ran E) \land b \in ω))$
56		simplr	$⊢ ((suc b \in ω \land \neg suc b \in ran E) \land b \in ω) \to \neg suc b \in ran E$
57	21	adantl	$⊢ ((suc b \in ω \land \neg suc b \in ran E) \land b \in ω) \to (b \in ran E \leftrightarrow \neg suc b \in ran E)$
58	56 57	mpbird	$⊢ ((suc b \in ω \land \neg suc b \in ran E) \land b \in ω) \to b \in ran E$
59	55 58	syl6bi	$⊢ a = suc b \to (((a \in ω \land \neg a \in ran E) \land b \in ω) \to b \in ran E)$
60	59	com12	$⊢ ((a \in ω \land \neg a \in ran E) \land b \in ω) \to (a = suc b \to b \in ran E)$
61	60	impr	$⊢ ((a \in ω \land \neg a \in ran E) \land (b \in ω \land a = suc b)) \to b \in ran E$
62		simprr	$⊢ ((a \in ω \land \neg a \in ran E) \land (b \in ω \land a = suc b)) \to a = suc b$
63	62	eqcomd	$⊢ ((a \in ω \land \neg a \in ran E) \land (b \in ω \land a = suc b)) \to suc b = a$
64	50 61 63	reximssdv	$⊢ (a \in ω \land \neg a \in ran E) \to \exists b \in ran E suc b = a$
65	30 64	impbii	$⊢ \exists b \in ran E suc b = a \leftrightarrow (a \in ω \land \neg a \in ran E)$
66	16 65	bitri	$⊢ \exists b \in ran E S (b) = a \leftrightarrow (a \in ω \land \neg a \in ran E)$
67		f1fn	$⊢ S : On \underset{1-1}{⟶} On \to S Fn On$
68	3 67	ax-mp	$⊢ S Fn On$
69		fvelimab	$⊢ (S Fn On \land ran E \subseteq On) \to (a \in S [ran E] \leftrightarrow \exists b \in ran E S (b) = a)$
70	68 9 69	mp2an	$⊢ a \in S [ran E] \leftrightarrow \exists b \in ran E S (b) = a$
71		eldif	$⊢ a \in (ω ∖ ran E) \leftrightarrow (a \in ω \land \neg a \in ran E)$
72	66 70 71	3bitr4i	$⊢ a \in S [ran E] \leftrightarrow a \in (ω ∖ ran E)$
73	72	eqriv	$⊢ S [ran E] = ω ∖ ran E$
74		f1oeq3	$⊢ S [ran E] = ω ∖ ran E \to (({S ↾}_{ran E}) : ran E \underset{1-1 onto}{⟶} S [ran E] \leftrightarrow ({S ↾}_{ran E}) : ran E \underset{1-1 onto}{⟶} ω ∖ ran E)$
75	73 74	ax-mp	$⊢ ({S ↾}_{ran E}) : ran E \underset{1-1 onto}{⟶} S [ran E] \leftrightarrow ({S ↾}_{ran E}) : ran E \underset{1-1 onto}{⟶} ω ∖ ran E$
76	11 75	mpbi	$⊢ ({S ↾}_{ran E}) : ran E \underset{1-1 onto}{⟶} ω ∖ ran E$

Metamath Proof Explorer

Theorem fin1a2lem6

Proof