cnfcom2

Description: Any nonzero ordinal B is equinumerous to the leading term of its Cantor normal form. (Contributed by Mario Carneiro, 30-May-2015) (Revised by AV, 3-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)$
	cnfcom2.1	$⊢ φ \to \emptyset \in B$
Assertion	cnfcom2	$⊢ φ \to T (dom G) : B \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (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		cnfcom2.1	$⊢ φ \to \emptyset \in B$
12		ovex	$⊢ F supp \emptyset \in V$
13	5	oion	$⊢ F supp \emptyset \in V \to dom G \in On$
14	12 13	ax-mp	$⊢ dom G \in On$
15	14	elexi	$⊢ dom G \in V$
16	15	uniex	$⊢ ⋃ dom G \in V$
17	16	sucid	$⊢ ⋃ dom G \in suc ⋃ dom G$
18	1 2 3 4 5 6 7 8 9 10 11	cnfcom2lem	$⊢ φ \to dom G = suc ⋃ dom G$
19	17 18	eleqtrrid	$⊢ φ \to ⋃ dom G \in dom G$
20	1 2 3 4 5 6 7 8 9 19	cnfcom	$⊢ φ \to T (suc ⋃ dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (⋃ dom G)) \cdot_{𝑜} F (G (⋃ dom G))$
21	10	oveq2i	$⊢ ω ↑_{𝑜} W = ω ↑_{𝑜} G (⋃ dom G)$
22	10	fveq2i	$⊢ F (W) = F (G (⋃ dom G))$
23	21 22	oveq12i	$⊢ (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) = (ω ↑_{𝑜} G (⋃ dom G)) \cdot_{𝑜} F (G (⋃ dom G))$
24		f1oeq3	$⊢ (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) = (ω ↑_{𝑜} G (⋃ dom G)) \cdot_{𝑜} F (G (⋃ dom G)) \to (T (suc ⋃ dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \leftrightarrow T (suc ⋃ dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (⋃ dom G)) \cdot_{𝑜} F (G (⋃ dom G)))$
25	23 24	ax-mp	$⊢ T (suc ⋃ dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \leftrightarrow T (suc ⋃ dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} G (⋃ dom G)) \cdot_{𝑜} F (G (⋃ dom G))$
26	20 25	sylibr	$⊢ φ \to T (suc ⋃ dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W)$
27	18	fveq2d	$⊢ φ \to T (dom G) = T (suc ⋃ dom G)$
28		f1oeq1	$⊢ T (dom G) = T (suc ⋃ dom G) \to (T (dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \leftrightarrow T (suc ⋃ dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W))$
29	27 28	syl	$⊢ φ \to (T (dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \leftrightarrow T (suc ⋃ dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W))$
30	26 29	mpbird	$⊢ φ \to T (dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W)$
31	4	fveq2i	$⊢ (ω CNF A) (F) = (ω CNF A) ({(ω CNF A)}^{-1} (B))$
32		omelon	$⊢ ω \in On$
33	32	a1i	$⊢ φ \to ω \in On$
34	1 33 2	cantnff1o	$⊢ φ \to (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A$
35		f1ocnv	$⊢ (ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S$
36		f1of	$⊢ {(ω CNF A)}^{-1} : ω ↑_{𝑜} A \underset{1-1 onto}{⟶} S \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
37	34 35 36	3syl	$⊢ φ \to {(ω CNF A)}^{-1} : ω ↑_{𝑜} A ⟶ S$
38	37 3	ffvelrnd	$⊢ φ \to {(ω CNF A)}^{-1} (B) \in S$
39	4 38	eqeltrid	$⊢ φ \to F \in S$
40	8	oveq1i	$⊢ M +_{𝑜} z = ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z$
41	40	a1i	$⊢ (k \in V \land z \in V) \to M +_{𝑜} z = ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z$
42	41	mpoeq3ia	$⊢ (k \in V, z \in V ⟼ M +_{𝑜} z) = (k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z)$
43		eqid	$⊢ \emptyset = \emptyset$
44		seqomeq12	$⊢ ((k \in V, z \in V ⟼ M +_{𝑜} z) = (k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z) \land \emptyset = \emptyset) \to {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
45	42 43 44	mp2an	$⊢ {seq}_{ω} ((k \in V, z \in V ⟼ M +_{𝑜} z), \emptyset) = {seq}_{ω} ((k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
46	6 45	eqtri	$⊢ H = {seq}_{ω} ((k \in V, z \in V ⟼ ((ω ↑_{𝑜} G (k)) \cdot_{𝑜} F (G (k))) +_{𝑜} z), \emptyset)$
47	1 33 2 5 39 46	cantnfval	$⊢ φ \to (ω CNF A) (F) = H (dom G)$
48	31 47	syl5reqr	$⊢ φ \to H (dom G) = (ω CNF A) ({(ω CNF A)}^{-1} (B))$
49	18	fveq2d	$⊢ φ \to H (dom G) = H (suc ⋃ dom G)$
50		f1ocnvfv2	$⊢ ((ω CNF A) : S \underset{1-1 onto}{⟶} ω ↑_{𝑜} A \land B \in (ω ↑_{𝑜} A)) \to (ω CNF A) ({(ω CNF A)}^{-1} (B)) = B$
51	34 3 50	syl2anc	$⊢ φ \to (ω CNF A) ({(ω CNF A)}^{-1} (B)) = B$
52	48 49 51	3eqtr3d	$⊢ φ \to H (suc ⋃ dom G) = B$
53	52	f1oeq2d	$⊢ φ \to (T (dom G) : H (suc ⋃ dom G) \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W) \leftrightarrow T (dom G) : B \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W))$
54	30 53	mpbid	$⊢ φ \to T (dom G) : B \underset{1-1 onto}{⟶} (ω ↑_{𝑜} W) \cdot_{𝑜} F (W)$

Metamath Proof Explorer

Theorem cnfcom2

Proof