ackbij2

Description: The Ackermann bijection, part 2: hereditarily finite sets can be represented by recursive binary notation. (Contributed by Stefan O'Rear, 18-Nov-2014)

	Ref	Expression
Hypotheses	ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
	ackbij.g	$⊢ G = (x \in V ⟼ (y \in 𝒫 dom x ⟼ F (x [y])))$
	ackbij.h	$⊢ H = ⋃ rec (G, \emptyset) [ω]$
Assertion	ackbij2	$⊢ H : ⋃ R_{1} [ω] \underset{1-1 onto}{⟶} ω$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$⊢ F = (x \in (𝒫 ω \cap Fin) ⟼ card (⋃_{y \in x} (\{y\} \times 𝒫 y)))$
2		ackbij.g	$⊢ G = (x \in V ⟼ (y \in 𝒫 dom x ⟼ F (x [y])))$
3		ackbij.h	$⊢ H = ⋃ rec (G, \emptyset) [ω]$
4		fveq2	$⊢ a = b \to rec (G, \emptyset) (a) = rec (G, \emptyset) (b)$
5		fvex	$⊢ rec (G, \emptyset) (a) \in V$
6	4 5	f1iun	$⊢ \forall a \in ω (rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1}{⟶} ω \land \forall b \in ω (rec (G, \emptyset) (a) \subseteq rec (G, \emptyset) (b) \lor rec (G, \emptyset) (b) \subseteq rec (G, \emptyset) (a))) \to ⋃_{a \in ω} rec (G, \emptyset) (a) : ⋃_{a \in ω} R_{1} (a) \underset{1-1}{⟶} ω$
7	1 2	ackbij2lem2	$⊢ a \in ω \to rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1 onto}{⟶} card (R_{1} (a))$
8		f1of1	$⊢ rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1 onto}{⟶} card (R_{1} (a)) \to rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1}{⟶} card (R_{1} (a))$
9	7 8	syl	$⊢ a \in ω \to rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1}{⟶} card (R_{1} (a))$
10		ordom	$⊢ Ord ω$
11		r1fin	$⊢ a \in ω \to R_{1} (a) \in Fin$
12		ficardom	$⊢ R_{1} (a) \in Fin \to card (R_{1} (a)) \in ω$
13	11 12	syl	$⊢ a \in ω \to card (R_{1} (a)) \in ω$
14		ordelss	$⊢ (Ord ω \land card (R_{1} (a)) \in ω) \to card (R_{1} (a)) \subseteq ω$
15	10 13 14	sylancr	$⊢ a \in ω \to card (R_{1} (a)) \subseteq ω$
16		f1ss	$⊢ (rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1}{⟶} card (R_{1} (a)) \land card (R_{1} (a)) \subseteq ω) \to rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1}{⟶} ω$
17	9 15 16	syl2anc	$⊢ a \in ω \to rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1}{⟶} ω$
18		nnord	$⊢ a \in ω \to Ord a$
19		nnord	$⊢ b \in ω \to Ord b$
20		ordtri2or2	$⊢ (Ord a \land Ord b) \to (a \subseteq b \lor b \subseteq a)$
21	18 19 20	syl2an	$⊢ (a \in ω \land b \in ω) \to (a \subseteq b \lor b \subseteq a)$
22	1 2	ackbij2lem4	$⊢ ((b \in ω \land a \in ω) \land a \subseteq b) \to rec (G, \emptyset) (a) \subseteq rec (G, \emptyset) (b)$
23	22	ex	$⊢ (b \in ω \land a \in ω) \to (a \subseteq b \to rec (G, \emptyset) (a) \subseteq rec (G, \emptyset) (b))$
24	23	ancoms	$⊢ (a \in ω \land b \in ω) \to (a \subseteq b \to rec (G, \emptyset) (a) \subseteq rec (G, \emptyset) (b))$
25	1 2	ackbij2lem4	$⊢ ((a \in ω \land b \in ω) \land b \subseteq a) \to rec (G, \emptyset) (b) \subseteq rec (G, \emptyset) (a)$
26	25	ex	$⊢ (a \in ω \land b \in ω) \to (b \subseteq a \to rec (G, \emptyset) (b) \subseteq rec (G, \emptyset) (a))$
27	24 26	orim12d	$⊢ (a \in ω \land b \in ω) \to ((a \subseteq b \lor b \subseteq a) \to (rec (G, \emptyset) (a) \subseteq rec (G, \emptyset) (b) \lor rec (G, \emptyset) (b) \subseteq rec (G, \emptyset) (a)))$
28	21 27	mpd	$⊢ (a \in ω \land b \in ω) \to (rec (G, \emptyset) (a) \subseteq rec (G, \emptyset) (b) \lor rec (G, \emptyset) (b) \subseteq rec (G, \emptyset) (a))$
29	28	ralrimiva	$⊢ a \in ω \to \forall b \in ω (rec (G, \emptyset) (a) \subseteq rec (G, \emptyset) (b) \lor rec (G, \emptyset) (b) \subseteq rec (G, \emptyset) (a))$
30	17 29	jca	$⊢ a \in ω \to (rec (G, \emptyset) (a) : R_{1} (a) \underset{1-1}{⟶} ω \land \forall b \in ω (rec (G, \emptyset) (a) \subseteq rec (G, \emptyset) (b) \lor rec (G, \emptyset) (b) \subseteq rec (G, \emptyset) (a)))$
31	6 30	mprg	$⊢ ⋃_{a \in ω} rec (G, \emptyset) (a) : ⋃_{a \in ω} R_{1} (a) \underset{1-1}{⟶} ω$
32		rdgfun	$⊢ Fun rec (G, \emptyset)$
33		funiunfv	$⊢ Fun rec (G, \emptyset) \to ⋃_{a \in ω} rec (G, \emptyset) (a) = ⋃ rec (G, \emptyset) [ω]$
34	33	eqcomd	$⊢ Fun rec (G, \emptyset) \to ⋃ rec (G, \emptyset) [ω] = ⋃_{a \in ω} rec (G, \emptyset) (a)$
35		f1eq1	$⊢ ⋃ rec (G, \emptyset) [ω] = ⋃_{a \in ω} rec (G, \emptyset) (a) \to (⋃ rec (G, \emptyset) [ω] : ⋃ R_{1} [ω] \underset{1-1}{⟶} ω \leftrightarrow ⋃_{a \in ω} rec (G, \emptyset) (a) : ⋃ R_{1} [ω] \underset{1-1}{⟶} ω)$
36	32 34 35	mp2b	$⊢ ⋃ rec (G, \emptyset) [ω] : ⋃ R_{1} [ω] \underset{1-1}{⟶} ω \leftrightarrow ⋃_{a \in ω} rec (G, \emptyset) (a) : ⋃ R_{1} [ω] \underset{1-1}{⟶} ω$
37		r1funlim	$⊢ (Fun R_{1} \land Lim dom R_{1})$
38	37	simpli	$⊢ Fun R_{1}$
39		funiunfv	$⊢ Fun R_{1} \to ⋃_{a \in ω} R_{1} (a) = ⋃ R_{1} [ω]$
40		f1eq2	$⊢ ⋃_{a \in ω} R_{1} (a) = ⋃ R_{1} [ω] \to (⋃_{a \in ω} rec (G, \emptyset) (a) : ⋃_{a \in ω} R_{1} (a) \underset{1-1}{⟶} ω \leftrightarrow ⋃_{a \in ω} rec (G, \emptyset) (a) : ⋃ R_{1} [ω] \underset{1-1}{⟶} ω)$
41	38 39 40	mp2b	$⊢ ⋃_{a \in ω} rec (G, \emptyset) (a) : ⋃_{a \in ω} R_{1} (a) \underset{1-1}{⟶} ω \leftrightarrow ⋃_{a \in ω} rec (G, \emptyset) (a) : ⋃ R_{1} [ω] \underset{1-1}{⟶} ω$
42	36 41	bitr4i	$⊢ ⋃ rec (G, \emptyset) [ω] : ⋃ R_{1} [ω] \underset{1-1}{⟶} ω \leftrightarrow ⋃_{a \in ω} rec (G, \emptyset) (a) : ⋃_{a \in ω} R_{1} (a) \underset{1-1}{⟶} ω$
43	31 42	mpbir	$⊢ ⋃ rec (G, \emptyset) [ω] : ⋃ R_{1} [ω] \underset{1-1}{⟶} ω$
44		rnuni	$⊢ ran ⋃ rec (G, \emptyset) [ω] = ⋃_{a \in rec (G, \emptyset) [ω]} ran a$
45		eliun	$⊢ b \in ⋃_{a \in rec (G, \emptyset) [ω]} ran a \leftrightarrow \exists a \in rec (G, \emptyset) [ω] b \in ran a$
46		df-rex	$⊢ \exists a \in rec (G, \emptyset) [ω] b \in ran a \leftrightarrow \exists a (a \in rec (G, \emptyset) [ω] \land b \in ran a)$
47		funfn	$⊢ Fun rec (G, \emptyset) \leftrightarrow rec (G, \emptyset) Fn dom rec (G, \emptyset)$
48	32 47	mpbi	$⊢ rec (G, \emptyset) Fn dom rec (G, \emptyset)$
49		rdgdmlim	$⊢ Lim dom rec (G, \emptyset)$
50		limomss	$⊢ Lim dom rec (G, \emptyset) \to ω \subseteq dom rec (G, \emptyset)$
51	49 50	ax-mp	$⊢ ω \subseteq dom rec (G, \emptyset)$
52		fvelimab	$⊢ (rec (G, \emptyset) Fn dom rec (G, \emptyset) \land ω \subseteq dom rec (G, \emptyset)) \to (a \in rec (G, \emptyset) [ω] \leftrightarrow \exists c \in ω rec (G, \emptyset) (c) = a)$
53	48 51 52	mp2an	$⊢ a \in rec (G, \emptyset) [ω] \leftrightarrow \exists c \in ω rec (G, \emptyset) (c) = a$
54	1 2	ackbij2lem2	$⊢ c \in ω \to rec (G, \emptyset) (c) : R_{1} (c) \underset{1-1 onto}{⟶} card (R_{1} (c))$
55		f1ofo	$⊢ rec (G, \emptyset) (c) : R_{1} (c) \underset{1-1 onto}{⟶} card (R_{1} (c)) \to rec (G, \emptyset) (c) : R_{1} (c) \underset{onto}{⟶} card (R_{1} (c))$
56		forn	$⊢ rec (G, \emptyset) (c) : R_{1} (c) \underset{onto}{⟶} card (R_{1} (c)) \to ran rec (G, \emptyset) (c) = card (R_{1} (c))$
57	54 55 56	3syl	$⊢ c \in ω \to ran rec (G, \emptyset) (c) = card (R_{1} (c))$
58		r1fin	$⊢ c \in ω \to R_{1} (c) \in Fin$
59		ficardom	$⊢ R_{1} (c) \in Fin \to card (R_{1} (c)) \in ω$
60	58 59	syl	$⊢ c \in ω \to card (R_{1} (c)) \in ω$
61		ordelss	$⊢ (Ord ω \land card (R_{1} (c)) \in ω) \to card (R_{1} (c)) \subseteq ω$
62	10 60 61	sylancr	$⊢ c \in ω \to card (R_{1} (c)) \subseteq ω$
63	57 62	eqsstrd	$⊢ c \in ω \to ran rec (G, \emptyset) (c) \subseteq ω$
64		rneq	$⊢ rec (G, \emptyset) (c) = a \to ran rec (G, \emptyset) (c) = ran a$
65	64	sseq1d	$⊢ rec (G, \emptyset) (c) = a \to (ran rec (G, \emptyset) (c) \subseteq ω \leftrightarrow ran a \subseteq ω)$
66	63 65	syl5ibcom	$⊢ c \in ω \to (rec (G, \emptyset) (c) = a \to ran a \subseteq ω)$
67	66	rexlimiv	$⊢ \exists c \in ω rec (G, \emptyset) (c) = a \to ran a \subseteq ω$
68	53 67	sylbi	$⊢ a \in rec (G, \emptyset) [ω] \to ran a \subseteq ω$
69	68	sselda	$⊢ (a \in rec (G, \emptyset) [ω] \land b \in ran a) \to b \in ω$
70	69	exlimiv	$⊢ \exists a (a \in rec (G, \emptyset) [ω] \land b \in ran a) \to b \in ω$
71		peano2	$⊢ b \in ω \to suc b \in ω$
72		fnfvima	$⊢ (rec (G, \emptyset) Fn dom rec (G, \emptyset) \land ω \subseteq dom rec (G, \emptyset) \land suc b \in ω) \to rec (G, \emptyset) (suc b) \in rec (G, \emptyset) [ω]$
73	48 51 71 72	mp3an12i	$⊢ b \in ω \to rec (G, \emptyset) (suc b) \in rec (G, \emptyset) [ω]$
74		vex	$⊢ b \in V$
75		cardnn	$⊢ suc b \in ω \to card (suc b) = suc b$
76		fvex	$⊢ R_{1} (suc b) \in V$
77	37	simpri	$⊢ Lim dom R_{1}$
78		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
79	77 78	ax-mp	$⊢ ω \subseteq dom R_{1}$
80	79	sseli	$⊢ suc b \in ω \to suc b \in dom R_{1}$
81		onssr1	$⊢ suc b \in dom R_{1} \to suc b \subseteq R_{1} (suc b)$
82	80 81	syl	$⊢ suc b \in ω \to suc b \subseteq R_{1} (suc b)$
83		ssdomg	$⊢ R_{1} (suc b) \in V \to (suc b \subseteq R_{1} (suc b) \to suc b ≼ R_{1} (suc b))$
84	76 82 83	mpsyl	$⊢ suc b \in ω \to suc b ≼ R_{1} (suc b)$
85		nnon	$⊢ suc b \in ω \to suc b \in On$
86		onenon	$⊢ suc b \in On \to suc b \in dom card$
87	85 86	syl	$⊢ suc b \in ω \to suc b \in dom card$
88		r1fin	$⊢ suc b \in ω \to R_{1} (suc b) \in Fin$
89		finnum	$⊢ R_{1} (suc b) \in Fin \to R_{1} (suc b) \in dom card$
90	88 89	syl	$⊢ suc b \in ω \to R_{1} (suc b) \in dom card$
91		carddom2	$⊢ (suc b \in dom card \land R_{1} (suc b) \in dom card) \to (card (suc b) \subseteq card (R_{1} (suc b)) \leftrightarrow suc b ≼ R_{1} (suc b))$
92	87 90 91	syl2anc	$⊢ suc b \in ω \to (card (suc b) \subseteq card (R_{1} (suc b)) \leftrightarrow suc b ≼ R_{1} (suc b))$
93	84 92	mpbird	$⊢ suc b \in ω \to card (suc b) \subseteq card (R_{1} (suc b))$
94	75 93	eqsstrrd	$⊢ suc b \in ω \to suc b \subseteq card (R_{1} (suc b))$
95	71 94	syl	$⊢ b \in ω \to suc b \subseteq card (R_{1} (suc b))$
96		sucssel	$⊢ b \in V \to (suc b \subseteq card (R_{1} (suc b)) \to b \in card (R_{1} (suc b)))$
97	74 95 96	mpsyl	$⊢ b \in ω \to b \in card (R_{1} (suc b))$
98	1 2	ackbij2lem2	$⊢ suc b \in ω \to rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b))$
99		f1ofo	$⊢ rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{1-1 onto}{⟶} card (R_{1} (suc b)) \to rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{onto}{⟶} card (R_{1} (suc b))$
100		forn	$⊢ rec (G, \emptyset) (suc b) : R_{1} (suc b) \underset{onto}{⟶} card (R_{1} (suc b)) \to ran rec (G, \emptyset) (suc b) = card (R_{1} (suc b))$
101	71 98 99 100	4syl	$⊢ b \in ω \to ran rec (G, \emptyset) (suc b) = card (R_{1} (suc b))$
102	97 101	eleqtrrd	$⊢ b \in ω \to b \in ran rec (G, \emptyset) (suc b)$
103		fvex	$⊢ rec (G, \emptyset) (suc b) \in V$
104		eleq1	$⊢ a = rec (G, \emptyset) (suc b) \to (a \in rec (G, \emptyset) [ω] \leftrightarrow rec (G, \emptyset) (suc b) \in rec (G, \emptyset) [ω])$
105		rneq	$⊢ a = rec (G, \emptyset) (suc b) \to ran a = ran rec (G, \emptyset) (suc b)$
106	105	eleq2d	$⊢ a = rec (G, \emptyset) (suc b) \to (b \in ran a \leftrightarrow b \in ran rec (G, \emptyset) (suc b))$
107	104 106	anbi12d	$⊢ a = rec (G, \emptyset) (suc b) \to ((a \in rec (G, \emptyset) [ω] \land b \in ran a) \leftrightarrow (rec (G, \emptyset) (suc b) \in rec (G, \emptyset) [ω] \land b \in ran rec (G, \emptyset) (suc b)))$
108	103 107	spcev	$⊢ (rec (G, \emptyset) (suc b) \in rec (G, \emptyset) [ω] \land b \in ran rec (G, \emptyset) (suc b)) \to \exists a (a \in rec (G, \emptyset) [ω] \land b \in ran a)$
109	73 102 108	syl2anc	$⊢ b \in ω \to \exists a (a \in rec (G, \emptyset) [ω] \land b \in ran a)$
110	70 109	impbii	$⊢ \exists a (a \in rec (G, \emptyset) [ω] \land b \in ran a) \leftrightarrow b \in ω$
111	45 46 110	3bitri	$⊢ b \in ⋃_{a \in rec (G, \emptyset) [ω]} ran a \leftrightarrow b \in ω$
112	111	eqriv	$⊢ ⋃_{a \in rec (G, \emptyset) [ω]} ran a = ω$
113	44 112	eqtri	$⊢ ran ⋃ rec (G, \emptyset) [ω] = ω$
114		dff1o5	$⊢ ⋃ rec (G, \emptyset) [ω] : ⋃ R_{1} [ω] \underset{1-1 onto}{⟶} ω \leftrightarrow (⋃ rec (G, \emptyset) [ω] : ⋃ R_{1} [ω] \underset{1-1}{⟶} ω \land ran ⋃ rec (G, \emptyset) [ω] = ω)$
115	43 113 114	mpbir2an	$⊢ ⋃ rec (G, \emptyset) [ω] : ⋃ R_{1} [ω] \underset{1-1 onto}{⟶} ω$
116		f1oeq1	$⊢ H = ⋃ rec (G, \emptyset) [ω] \to (H : ⋃ R_{1} [ω] \underset{1-1 onto}{⟶} ω \leftrightarrow ⋃ rec (G, \emptyset) [ω] : ⋃ R_{1} [ω] \underset{1-1 onto}{⟶} ω)$
117	3 116	ax-mp	$⊢ H : ⋃ R_{1} [ω] \underset{1-1 onto}{⟶} ω \leftrightarrow ⋃ rec (G, \emptyset) [ω] : ⋃ R_{1} [ω] \underset{1-1 onto}{⟶} ω$
118	115 117	mpbir	$⊢ H : ⋃ R_{1} [ω] \underset{1-1 onto}{⟶} ω$

Metamath Proof Explorer

Theorem ackbij2

Proof