cnfcom3

Description: Any infinite ordinal B is equinumerous to a power of _om . (We are being careful here to show explicit bijections rather than simple equinumerosity because we want a uniform construction for cnfcom3c .) (Contributed by Mario Carneiro, 28-May-2015) (Revised by AV, 4-Jul-2019)

	Ref	Expression
Hypotheses	cnfcom.s	$⊢ S = dom (ω CNF A)$
	cnfcom.a	$⊢ φ \to A \in On$
	cnfcom.b	$⊢ φ \to B \in (ω ↑_{𝑜} A)$
	cnfcom.f	$⊢ F = {(ω CNF A)}^{-1} (B)$
	cnfcom.g	$⊢ G = OrdIso (E, F supp \emptyset)$
	cnfcom.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
	cnfcom.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
	cnfcom.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
	cnfcom.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
	cnfcom.w	$⊢ W = G (⋃ dom G)$
	cnfcom3.1	$⊢ φ \to ω \subseteq B$
	cnfcom.x	$⊢ X = (u \in F (W), v \in (ω ↑_{𝑜} W) ⟼ (F (W) \cdot_{𝑜} v) +_{𝑜} u)$
	cnfcom.y	$⊢ Y = (u \in F (W), v \in (ω ↑_{𝑜} W) ⟼ ((ω ↑_{𝑜} W) \cdot_{𝑜} u) +_{𝑜} v)$
	cnfcom.n	$⊢ N = (X \circ Y^{-1}) \circ T (dom G)$
Assertion	cnfcom3	$⊢ φ \to N : B \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$

Proof

Step	Hyp	Ref	Expression
1		cnfcom.s	$⊢ S = dom (ω CNF A)$
2		cnfcom.a	$⊢ φ \to A \in On$
3		cnfcom.b	$⊢ φ \to B \in (ω ↑_{𝑜} A)$
4		cnfcom.f	$⊢ F = {(ω CNF A)}^{-1} (B)$
5		cnfcom.g	$⊢ G = OrdIso (E, F supp \emptyset)$
6		cnfcom.h	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset)$
7		cnfcom.t	$⊢ T = {seq}_{ω} ((k \in V, f \in V ⟼ K), \emptyset)$
8		cnfcom.m	$⊢ M = (ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))$
9		cnfcom.k	$⊢ K = (x \in M ⟼ dom f +_{𝑜} x) \cup {(x \in dom f ⟼ M +_{𝑜} x)}^{-1}$
10		cnfcom.w	$⊢ W = G (⋃ dom G)$
11		cnfcom3.1	$⊢ φ \to ω \subseteq B$
12		cnfcom.x	$⊢ X = (u \in F (W), v \in (ω ↑_{𝑜} W) ⟼ (F (W) \cdot_{𝑜} v) +_{𝑜} u)$
13		cnfcom.y	$⊢ Y = (u \in F (W), v \in (ω ↑_{𝑜} W) ⟼ ((ω ↑_{𝑜} W) \cdot_{𝑜} u) +_{𝑜} v)$
14		cnfcom.n	$⊢ N = (X \circ Y^{-1}) \circ T (dom G)$
15		omelon	$⊢ ω \in On$
16		suppssdm	$⊢ F supp \emptyset \subseteq dom F$
17	15	a1i	$⊢ φ \to ω \in On$
18	1 17 2	cantnff1o	$⊢ φ \to (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A$
19		f1ocnv	$⊢ (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S$
20		f1of	$⊢ {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
21	18 19 20	3syl	$⊢ φ \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
22	21 3	ffvelcdmd	$⊢ φ \to {(ω CNF A)}^{-1} (B) \in S$
23	4 22	eqeltrid	$⊢ φ \to F \in S$
24	1 17 2	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : A ⟶ ω \land {finSupp}_{\emptyset} (F)))$
25	23 24	mpbid	$⊢ φ \to (F : A ⟶ ω \land {finSupp}_{\emptyset} (F))$
26	25	simpld	$⊢ φ \to F : A ⟶ ω$
27	16 26	fssdm	$⊢ φ \to F supp \emptyset \subseteq A$
28		ovex	$⊢ F supp \emptyset \in V$
29	5	oion	$⊢ F supp \emptyset \in V \to dom G \in On$
30	28 29	ax-mp	$⊢ dom G \in On$
31	30	elexi	$⊢ dom G \in V$
32	31	uniex	$⊢ ⋃ dom G \in V$
33	32	sucid	$⊢ ⋃ dom G \in suc ⋃ dom G$
34		peano1	$⊢ \emptyset \in ω$
35	34	a1i	$⊢ φ \to \emptyset \in ω$
36	11 35	sseldd	$⊢ φ \to \emptyset \in B$
37	1 2 3 4 5 6 7 8 9 10 36	cnfcom2lem	$⊢ φ \to dom G = suc ⋃ dom G$
38	33 37	eleqtrrid	$⊢ φ \to ⋃ dom G \in dom G$
39	5	oif	$⊢ G : dom G ⟶ F supp \emptyset$
40	39	ffvelcdmi	$⊢ ⋃ dom G \in dom G \to G (⋃ dom G) \in {supp}_{\emptyset} (F)$
41	38 40	syl	$⊢ φ \to G (⋃ dom G) \in {supp}_{\emptyset} (F)$
42	10 41	eqeltrid	$⊢ φ \to W \in {supp}_{\emptyset} (F)$
43	27 42	sseldd	$⊢ φ \to W \in A$
44		onelon	$⊢ (A \in On \land W \in A) \to W \in On$
45	2 43 44	syl2anc	$⊢ φ \to W \in On$
46		oecl	$⊢ (ω \in On \land W \in On) \to ω ↑_{𝑜} W \in On$
47	15 45 46	sylancr	$⊢ φ \to ω ↑_{𝑜} W \in On$
48	26 43	ffvelcdmd	$⊢ φ \to F (W) \in ω$
49		nnon	$⊢ F (W) \in ω \to F (W) \in On$
50	48 49	syl	$⊢ φ \to F (W) \in On$
51	13 12	omf1o	$⊢ (ω ↑_{𝑜} W \in On \land F (W) \in On) \to (X \circ Y^{-1}) : (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \underset{1-1 onto}{⟶} F (W) \cdot_{𝑜} (ω ↑_{𝑜} W)$
52	47 50 51	syl2anc	$⊢ φ \to (X \circ Y^{-1}) : (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \underset{1-1 onto}{⟶} F (W) \cdot_{𝑜} (ω ↑_{𝑜} W)$
53	26	ffnd	$⊢ φ \to F Fn A$
54		0ex	$⊢ \emptyset \in V$
55	54	a1i	$⊢ φ \to \emptyset \in V$
56		elsuppfn	$⊢ (F Fn A \land A \in On \land \emptyset \in V) \to (W \in {supp}_{\emptyset} (F) \leftrightarrow (W \in A \land F (W) \neq \emptyset))$
57	53 2 55 56	syl3anc	$⊢ φ \to (W \in {supp}_{\emptyset} (F) \leftrightarrow (W \in A \land F (W) \neq \emptyset))$
58		simpr	$⊢ (W \in A \land F (W) \neq \emptyset) \to F (W) \neq \emptyset$
59	57 58	biimtrdi	$⊢ φ \to (W \in {supp}_{\emptyset} (F) \to F (W) \neq \emptyset)$
60	42 59	mpd	$⊢ φ \to F (W) \neq \emptyset$
61		on0eln0	$⊢ F (W) \in On \to (\emptyset \in F (W) \leftrightarrow F (W) \neq \emptyset)$
62	48 49 61	3syl	$⊢ φ \to (\emptyset \in F (W) \leftrightarrow F (W) \neq \emptyset)$
63	60 62	mpbird	$⊢ φ \to \emptyset \in F (W)$
64	1 2 3 4 5 6 7 8 9 10 11	cnfcom3lem	$⊢ φ \to W \in (On ∖ 1_{𝑜})$
65		ondif1	$⊢ W \in (On ∖ 1_{𝑜}) \leftrightarrow (W \in On \land \emptyset \in W)$
66	65	simprbi	$⊢ W \in (On ∖ 1_{𝑜}) \to \emptyset \in W$
67	64 66	syl	$⊢ φ \to \emptyset \in W$
68		omabs	$⊢ ((F (W) \in ω \land \emptyset \in F (W)) \land (W \in On \land \emptyset \in W)) \to F (W) \cdot_{𝑜} (ω ↑_{𝑜} W) = ω ↑_{𝑜} W$
69	48 63 45 67 68	syl22anc	$⊢ φ \to F (W) \cdot_{𝑜} (ω ↑_{𝑜} W) = ω ↑_{𝑜} W$
70	69	f1oeq3d	$⊢ φ \to ((X \circ Y^{-1}) : (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \underset{1-1 onto}{⟶} F (W) \cdot_{𝑜} (ω ↑_{𝑜} W) \leftrightarrow (X \circ Y^{-1}) : (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$
71	52 70	mpbid	$⊢ φ \to (X \circ Y^{-1}) : (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
72	1 2 3 4 5 6 7 8 9 10 36	cnfcom2	$⊢ φ \to T (dom G) : B \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W)$
73		f1oco	$⊢ ((X \circ Y^{-1}) : (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \land T (dom G) : B \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W)) \to ((X \circ Y^{-1}) \circ T (dom G)) : B \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
74	71 72 73	syl2anc	$⊢ φ \to ((X \circ Y^{-1}) \circ T (dom G)) : B \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
75		f1oeq1	$⊢ N = (X \circ Y^{-1}) \circ T (dom G) \to (N : B \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \leftrightarrow ((X \circ Y^{-1}) \circ T (dom G)) : B \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$
76	14 75	ax-mp	$⊢ N : B \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \leftrightarrow ((X \circ Y^{-1}) \circ T (dom G)) : B \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$
77	74 76	sylibr	$⊢ φ \to N : B \underset{1-1 onto}{⟶} ω ↑_{𝑜} W$

Metamath Proof Explorer

Theorem cnfcom3

Proof