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) Restate using the defined HF symbol. (Revised by Eric Schmidt, 24-Sep-2026)

	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	Could not format assertion : No typesetting found for \|- H : HF -1-1-onto-> _om with typecode \|-

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	Could not format ( U. ( rec ( G , (/) ) " _om ) = U_ a e. _om ( rec ( G , (/) ) ` a ) -> ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) ) : No typesetting found for \|- ( U. ( rec ( G , (/) ) " _om ) = U_ a e. _om ( rec ( G , (/) ) ` a ) -> ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) ) with typecode \|-
36	32 34 35	mp2b	Could not format ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) : No typesetting found for \|- ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) with typecode \|-
37		r1fun	$⊢ Fun R_{1}$
38		funiunfv	$⊢ Fun R_{1} \to ⋃_{a \in ω} R_{1} (a) = ⋃ R_{1} [ω]$
39		df-hf	Could not format HF = U. ( R1 " _om ) : No typesetting found for \|- HF = U. ( R1 " _om ) with typecode \|-
40	38 39	eqtr4di	Could not format ( Fun R1 -> U_ a e. _om ( R1 ` a ) = HF ) : No typesetting found for \|- ( Fun R1 -> U_ a e. _om ( R1 ` a ) = HF ) with typecode \|-
41		f1eq2	Could not format ( U_ a e. _om ( R1 ` a ) = HF -> ( U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) ) : No typesetting found for \|- ( U_ a e. _om ( R1 ` a ) = HF -> ( U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) ) with typecode \|-
42	37 40 41	mp2b	Could not format ( U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) : No typesetting found for \|- ( U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : HF -1-1-> _om ) with typecode \|-
43	36 42	bitr4i	Could not format ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om ) : No typesetting found for \|- ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om <-> U_ a e. _om ( rec ( G , (/) ) ` a ) : U_ a e. _om ( R1 ` a ) -1-1-> _om ) with typecode \|-
44	31 43	mpbir	Could not format U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om : No typesetting found for \|- U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om with typecode \|-
45		rnuni	$⊢ ran ⋃ rec (G, \emptyset) [ω] = ⋃_{a \in rec (G, \emptyset) [ω]} ran a$
46		eliun	$⊢ b \in ⋃_{a \in rec (G, \emptyset) [ω]} ran a \leftrightarrow \exists a \in rec (G, \emptyset) [ω] b \in ran a$
47		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)$
48		funfn	$⊢ Fun rec (G, \emptyset) \leftrightarrow rec (G, \emptyset) Fn dom rec (G, \emptyset)$
49	32 48	mpbi	$⊢ rec (G, \emptyset) Fn dom rec (G, \emptyset)$
50		rdgdmlim	$⊢ Lim dom rec (G, \emptyset)$
51		limomss	$⊢ Lim dom rec (G, \emptyset) \to ω \subseteq dom rec (G, \emptyset)$
52	50 51	ax-mp	$⊢ ω \subseteq dom rec (G, \emptyset)$
53		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)$
54	49 52 53	mp2an	$⊢ a \in rec (G, \emptyset) [ω] \leftrightarrow \exists c \in ω rec (G, \emptyset) (c) = a$
55	1 2	ackbij2lem2	$⊢ c \in ω \to rec (G, \emptyset) (c) : R_{1} (c) \underset{1-1 onto}{⟶} card (R_{1} (c))$
56		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))$
57		forn	$⊢ rec (G, \emptyset) (c) : R_{1} (c) \underset{onto}{⟶} card (R_{1} (c)) \to ran rec (G, \emptyset) (c) = card (R_{1} (c))$
58	55 56 57	3syl	$⊢ c \in ω \to ran rec (G, \emptyset) (c) = card (R_{1} (c))$
59		r1fin	$⊢ c \in ω \to R_{1} (c) \in Fin$
60		ficardom	$⊢ R_{1} (c) \in Fin \to card (R_{1} (c)) \in ω$
61	59 60	syl	$⊢ c \in ω \to card (R_{1} (c)) \in ω$
62		ordelss	$⊢ (Ord ω \land card (R_{1} (c)) \in ω) \to card (R_{1} (c)) \subseteq ω$
63	10 61 62	sylancr	$⊢ c \in ω \to card (R_{1} (c)) \subseteq ω$
64	58 63	eqsstrd	$⊢ c \in ω \to ran rec (G, \emptyset) (c) \subseteq ω$
65		rneq	$⊢ rec (G, \emptyset) (c) = a \to ran rec (G, \emptyset) (c) = ran a$
66	65	sseq1d	$⊢ rec (G, \emptyset) (c) = a \to (ran rec (G, \emptyset) (c) \subseteq ω \leftrightarrow ran a \subseteq ω)$
67	64 66	syl5ibcom	$⊢ c \in ω \to (rec (G, \emptyset) (c) = a \to ran a \subseteq ω)$
68	67	rexlimiv	$⊢ \exists c \in ω rec (G, \emptyset) (c) = a \to ran a \subseteq ω$
69	54 68	sylbi	$⊢ a \in rec (G, \emptyset) [ω] \to ran a \subseteq ω$
70	69	sselda	$⊢ (a \in rec (G, \emptyset) [ω] \land b \in ran a) \to b \in ω$
71	70	exlimiv	$⊢ \exists a (a \in rec (G, \emptyset) [ω] \land b \in ran a) \to b \in ω$
72		peano2	$⊢ b \in ω \to suc b \in ω$
73		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) [ω]$
74	49 52 72 73	mp3an12i	$⊢ b \in ω \to rec (G, \emptyset) (suc b) \in rec (G, \emptyset) [ω]$
75		vex	$⊢ b \in V$
76		cardnn	$⊢ suc b \in ω \to card (suc b) = suc b$
77		fvex	$⊢ R_{1} (suc b) \in V$
78		r1dmlim	$⊢ Lim dom R_{1}$
79		limomss	$⊢ Lim dom R_{1} \to ω \subseteq dom R_{1}$
80	78 79	ax-mp	$⊢ ω \subseteq dom R_{1}$
81	80	sseli	$⊢ suc b \in ω \to suc b \in dom R_{1}$
82		onssr1	$⊢ suc b \in dom R_{1} \to suc b \subseteq R_{1} (suc b)$
83	81 82	syl	$⊢ suc b \in ω \to suc b \subseteq R_{1} (suc b)$
84		ssdomg	$⊢ R_{1} (suc b) \in V \to (suc b \subseteq R_{1} (suc b) \to suc b ≼ R_{1} (suc b))$
85	77 83 84	mpsyl	$⊢ suc b \in ω \to suc b ≼ R_{1} (suc b)$
86		nnon	$⊢ suc b \in ω \to suc b \in On$
87		onenon	$⊢ suc b \in On \to suc b \in dom card$
88	86 87	syl	$⊢ suc b \in ω \to suc b \in dom card$
89		r1fin	$⊢ suc b \in ω \to R_{1} (suc b) \in Fin$
90		finnum	$⊢ R_{1} (suc b) \in Fin \to R_{1} (suc b) \in dom card$
91	89 90	syl	$⊢ suc b \in ω \to R_{1} (suc b) \in dom card$
92		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))$
93	88 91 92	syl2anc	$⊢ suc b \in ω \to (card (suc b) \subseteq card (R_{1} (suc b)) \leftrightarrow suc b ≼ R_{1} (suc b))$
94	85 93	mpbird	$⊢ suc b \in ω \to card (suc b) \subseteq card (R_{1} (suc b))$
95	76 94	eqsstrrd	$⊢ suc b \in ω \to suc b \subseteq card (R_{1} (suc b))$
96	72 95	syl	$⊢ b \in ω \to suc b \subseteq card (R_{1} (suc b))$
97		sucssel	$⊢ b \in V \to (suc b \subseteq card (R_{1} (suc b)) \to b \in card (R_{1} (suc b)))$
98	75 96 97	mpsyl	$⊢ b \in ω \to b \in card (R_{1} (suc b))$
99	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))$
100		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))$
101		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))$
102	72 99 100 101	4syl	$⊢ b \in ω \to ran rec (G, \emptyset) (suc b) = card (R_{1} (suc b))$
103	98 102	eleqtrrd	$⊢ b \in ω \to b \in ran rec (G, \emptyset) (suc b)$
104		fvex	$⊢ rec (G, \emptyset) (suc b) \in V$
105		eleq1	$⊢ a = rec (G, \emptyset) (suc b) \to (a \in rec (G, \emptyset) [ω] \leftrightarrow rec (G, \emptyset) (suc b) \in rec (G, \emptyset) [ω])$
106		rneq	$⊢ a = rec (G, \emptyset) (suc b) \to ran a = ran rec (G, \emptyset) (suc b)$
107	106	eleq2d	$⊢ a = rec (G, \emptyset) (suc b) \to (b \in ran a \leftrightarrow b \in ran rec (G, \emptyset) (suc b))$
108	105 107	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)))$
109	104 108	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)$
110	74 103 109	syl2anc	$⊢ b \in ω \to \exists a (a \in rec (G, \emptyset) [ω] \land b \in ran a)$
111	71 110	impbii	$⊢ \exists a (a \in rec (G, \emptyset) [ω] \land b \in ran a) \leftrightarrow b \in ω$
112	46 47 111	3bitri	$⊢ b \in ⋃_{a \in rec (G, \emptyset) [ω]} ran a \leftrightarrow b \in ω$
113	112	eqriv	$⊢ ⋃_{a \in rec (G, \emptyset) [ω]} ran a = ω$
114	45 113	eqtri	$⊢ ran ⋃ rec (G, \emptyset) [ω] = ω$
115		dff1o5	Could not format ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om <-> ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om /\ ran U. ( rec ( G , (/) ) " _om ) = _om ) ) : No typesetting found for \|- ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om <-> ( U. ( rec ( G , (/) ) " _om ) : HF -1-1-> _om /\ ran U. ( rec ( G , (/) ) " _om ) = _om ) ) with typecode \|-
116	44 114 115	mpbir2an	Could not format U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om : No typesetting found for \|- U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om with typecode \|-
117		f1oeq1	Could not format ( H = U. ( rec ( G , (/) ) " _om ) -> ( H : HF -1-1-onto-> _om <-> U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om ) ) : No typesetting found for \|- ( H = U. ( rec ( G , (/) ) " _om ) -> ( H : HF -1-1-onto-> _om <-> U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om ) ) with typecode \|-
118	3 117	ax-mp	Could not format ( H : HF -1-1-onto-> _om <-> U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om ) : No typesetting found for \|- ( H : HF -1-1-onto-> _om <-> U. ( rec ( G , (/) ) " _om ) : HF -1-1-onto-> _om ) with typecode \|-
119	116 118	mpbir	Could not format H : HF -1-1-onto-> _om : No typesetting found for \|- H : HF -1-1-onto-> _om with typecode \|-

Metamath Proof Explorer

Theorem ackbij2

Proof