fin23lem27

Description: The mapping constructed in fin23lem22 is in fact an isomorphism. (Contributed by Stefan O'Rear, 2-Nov-2014)

		Ref	Expression
	Hypothesis	fin23lem22.b	$⊢ C = (i \in ω ⟼ (ι j \in S \| (j \cap S) \approx i))$
	Assertion	fin23lem27	$⊢ (S \subseteq ω \land \neg S \in Fin) \to C {Isom}_{E, E} (ω, S)$

Proof

Step	Hyp	Ref	Expression
1		fin23lem22.b	$⊢ C = (i \in ω ⟼ (ι j \in S \| (j \cap S) \approx i))$
2		ordom	$⊢ Ord ω$
3		ordwe	$⊢ Ord ω \to E We ω$
4		weso	$⊢ E We ω \to E Or ω$
5	2 3 4	mp2b	$⊢ E Or ω$
6	5	a1i	$⊢ (S \subseteq ω \land \neg S \in Fin) \to E Or ω$
7		sopo	$⊢ E Or ω \to E Po ω$
8	5 7	ax-mp	$⊢ E Po ω$
9		poss	$⊢ S \subseteq ω \to (E Po ω \to E Po S)$
10	8 9	mpi	$⊢ S \subseteq ω \to E Po S$
11	10	adantr	$⊢ (S \subseteq ω \land \neg S \in Fin) \to E Po S$
12	1	fin23lem22	$⊢ (S \subseteq ω \land \neg S \in Fin) \to C : ω \underset{1-1 onto}{⟶} S$
13		f1ofo	$⊢ C : ω \underset{1-1 onto}{⟶} S \to C : ω \underset{onto}{⟶} S$
14	12 13	syl	$⊢ (S \subseteq ω \land \neg S \in Fin) \to C : ω \underset{onto}{⟶} S$
15		nnsdomel	$⊢ (a \in ω \land b \in ω) \to (a \in b \leftrightarrow a ≺ b)$
16	15	adantl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (a \in b \leftrightarrow a ≺ b)$
17	16	biimpd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (a \in b \to a ≺ b)$
18		fin23lem23	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land a \in ω) \to \exists! j \in S (j \cap S) \approx a$
19	18	adantrr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to \exists! j \in S (j \cap S) \approx a$
20		ineq1	$⊢ j = i \to j \cap S = i \cap S$
21	20	breq1d	$⊢ j = i \to ((j \cap S) \approx a \leftrightarrow (i \cap S) \approx a)$
22	21	cbvreuvw	$⊢ \exists! j \in S (j \cap S) \approx a \leftrightarrow \exists! i \in S (i \cap S) \approx a$
23	19 22	sylib	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to \exists! i \in S (i \cap S) \approx a$
24		nfv	$⊢ Ⅎ i ((ι j \in S \| (j \cap S) \approx a) \cap S) \approx a$
25	21	cbvriotavw	$⊢ (ι j \in S \| (j \cap S) \approx a) = (ι i \in S \| (i \cap S) \approx a)$
26		ineq1	$⊢ i = (ι j \in S \| (j \cap S) \approx a) \to i \cap S = (ι j \in S \| (j \cap S) \approx a) \cap S$
27	26	breq1d	$⊢ i = (ι j \in S \| (j \cap S) \approx a) \to ((i \cap S) \approx a \leftrightarrow ((ι j \in S \| (j \cap S) \approx a) \cap S) \approx a)$
28	24 25 27	riotaprop	$⊢ \exists! i \in S (i \cap S) \approx a \to ((ι j \in S \| (j \cap S) \approx a) \in S \land ((ι j \in S \| (j \cap S) \approx a) \cap S) \approx a)$
29	23 28	syl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to ((ι j \in S \| (j \cap S) \approx a) \in S \land ((ι j \in S \| (j \cap S) \approx a) \cap S) \approx a)$
30	29	simprd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to ((ι j \in S \| (j \cap S) \approx a) \cap S) \approx a$
31	30	adantrr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land ((a \in ω \land b \in ω) \land a ≺ b)) \to ((ι j \in S \| (j \cap S) \approx a) \cap S) \approx a$
32		simprr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land ((a \in ω \land b \in ω) \land a ≺ b)) \to a ≺ b$
33		fin23lem23	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land b \in ω) \to \exists! j \in S (j \cap S) \approx b$
34	33	adantrl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to \exists! j \in S (j \cap S) \approx b$
35	20	breq1d	$⊢ j = i \to ((j \cap S) \approx b \leftrightarrow (i \cap S) \approx b)$
36	35	cbvreuvw	$⊢ \exists! j \in S (j \cap S) \approx b \leftrightarrow \exists! i \in S (i \cap S) \approx b$
37	34 36	sylib	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to \exists! i \in S (i \cap S) \approx b$
38		nfv	$⊢ Ⅎ i ((ι j \in S \| (j \cap S) \approx b) \cap S) \approx b$
39	35	cbvriotavw	$⊢ (ι j \in S \| (j \cap S) \approx b) = (ι i \in S \| (i \cap S) \approx b)$
40		ineq1	$⊢ i = (ι j \in S \| (j \cap S) \approx b) \to i \cap S = (ι j \in S \| (j \cap S) \approx b) \cap S$
41	40	breq1d	$⊢ i = (ι j \in S \| (j \cap S) \approx b) \to ((i \cap S) \approx b \leftrightarrow ((ι j \in S \| (j \cap S) \approx b) \cap S) \approx b)$
42	38 39 41	riotaprop	$⊢ \exists! i \in S (i \cap S) \approx b \to ((ι j \in S \| (j \cap S) \approx b) \in S \land ((ι j \in S \| (j \cap S) \approx b) \cap S) \approx b)$
43	37 42	syl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to ((ι j \in S \| (j \cap S) \approx b) \in S \land ((ι j \in S \| (j \cap S) \approx b) \cap S) \approx b)$
44	43	simprd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to ((ι j \in S \| (j \cap S) \approx b) \cap S) \approx b$
45	44	ensymd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to b \approx ((ι j \in S \| (j \cap S) \approx b) \cap S)$
46	45	adantrr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land ((a \in ω \land b \in ω) \land a ≺ b)) \to b \approx ((ι j \in S \| (j \cap S) \approx b) \cap S)$
47		sdomentr	$⊢ (a ≺ b \land b \approx ((ι j \in S \| (j \cap S) \approx b) \cap S)) \to a ≺ ((ι j \in S \| (j \cap S) \approx b) \cap S)$
48	32 46 47	syl2anc	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land ((a \in ω \land b \in ω) \land a ≺ b)) \to a ≺ ((ι j \in S \| (j \cap S) \approx b) \cap S)$
49		ensdomtr	$⊢ (((ι j \in S \| (j \cap S) \approx a) \cap S) \approx a \land a ≺ ((ι j \in S \| (j \cap S) \approx b) \cap S)) \to ((ι j \in S \| (j \cap S) \approx a) \cap S) ≺ ((ι j \in S \| (j \cap S) \approx b) \cap S)$
50	31 48 49	syl2anc	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land ((a \in ω \land b \in ω) \land a ≺ b)) \to ((ι j \in S \| (j \cap S) \approx a) \cap S) ≺ ((ι j \in S \| (j \cap S) \approx b) \cap S)$
51	50	expr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (a ≺ b \to ((ι j \in S \| (j \cap S) \approx a) \cap S) ≺ ((ι j \in S \| (j \cap S) \approx b) \cap S))$
52		simpll	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to S \subseteq ω$
53		omsson	$⊢ ω \subseteq On$
54	52 53	sstrdi	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to S \subseteq On$
55	29	simpld	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (ι j \in S \| (j \cap S) \approx a) \in S$
56	54 55	sseldd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (ι j \in S \| (j \cap S) \approx a) \in On$
57	43	simpld	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (ι j \in S \| (j \cap S) \approx b) \in S$
58	54 57	sseldd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (ι j \in S \| (j \cap S) \approx b) \in On$
59		onsdominel	$⊢ ((ι j \in S \| (j \cap S) \approx a) \in On \land (ι j \in S \| (j \cap S) \approx b) \in On \land ((ι j \in S \| (j \cap S) \approx a) \cap S) ≺ ((ι j \in S \| (j \cap S) \approx b) \cap S)) \to (ι j \in S \| (j \cap S) \approx a) \in (ι j \in S \| (j \cap S) \approx b)$
60	59	3expia	$⊢ ((ι j \in S \| (j \cap S) \approx a) \in On \land (ι j \in S \| (j \cap S) \approx b) \in On) \to (((ι j \in S \| (j \cap S) \approx a) \cap S) ≺ ((ι j \in S \| (j \cap S) \approx b) \cap S) \to (ι j \in S \| (j \cap S) \approx a) \in (ι j \in S \| (j \cap S) \approx b))$
61	56 58 60	syl2anc	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (((ι j \in S \| (j \cap S) \approx a) \cap S) ≺ ((ι j \in S \| (j \cap S) \approx b) \cap S) \to (ι j \in S \| (j \cap S) \approx a) \in (ι j \in S \| (j \cap S) \approx b))$
62	17 51 61	3syld	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (a \in b \to (ι j \in S \| (j \cap S) \approx a) \in (ι j \in S \| (j \cap S) \approx b))$
63		breq2	$⊢ i = a \to ((j \cap S) \approx i \leftrightarrow (j \cap S) \approx a)$
64	63	riotabidv	$⊢ i = a \to (ι j \in S \| (j \cap S) \approx i) = (ι j \in S \| (j \cap S) \approx a)$
65		simprl	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to a \in ω$
66	1 64 65 55	fvmptd3	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to C (a) = (ι j \in S \| (j \cap S) \approx a)$
67		breq2	$⊢ i = b \to ((j \cap S) \approx i \leftrightarrow (j \cap S) \approx b)$
68	67	riotabidv	$⊢ i = b \to (ι j \in S \| (j \cap S) \approx i) = (ι j \in S \| (j \cap S) \approx b)$
69		simprr	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to b \in ω$
70	1 68 69 57	fvmptd3	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to C (b) = (ι j \in S \| (j \cap S) \approx b)$
71	66 70	eleq12d	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (C (a) \in C (b) \leftrightarrow (ι j \in S \| (j \cap S) \approx a) \in (ι j \in S \| (j \cap S) \approx b))$
72	62 71	sylibrd	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (a \in b \to C (a) \in C (b))$
73		epel	$⊢ a E b \leftrightarrow a \in b$
74		fvex	$⊢ C (b) \in V$
75	74	epeli	$⊢ C (a) E C (b) \leftrightarrow C (a) \in C (b)$
76	72 73 75	3imtr4g	$⊢ ((S \subseteq ω \land \neg S \in Fin) \land (a \in ω \land b \in ω)) \to (a E b \to C (a) E C (b))$
77	76	ralrimivva	$⊢ (S \subseteq ω \land \neg S \in Fin) \to \forall a \in ω \forall b \in ω (a E b \to C (a) E C (b))$
78		soisoi	$⊢ ((E Or ω \land E Po S) \land (C : ω \underset{onto}{⟶} S \land \forall a \in ω \forall b \in ω (a E b \to C (a) E C (b)))) \to C {Isom}_{E, E} (ω, S)$
79	6 11 14 77 78	syl22anc	$⊢ (S \subseteq ω \land \neg S \in Fin) \to C {Isom}_{E, E} (ω, S)$

Metamath Proof Explorer

Theorem fin23lem27

Proof