Theorem jf1o

Description: _J is a bijection from ( ( On X. On ) X. 9o ) to On . Proposition 15.3 of TakeutiZaring p. 155. (Contributed by BTernaryTau, 6-Oct-2026)

	Ref	Expression
Assertion	jf1o	⊢ 𝐽 : ( ( On × On ) × 9o ) –1-1-onto→ On

Proof

Step	Hyp	Ref	Expression
1		jf1	⊢ 𝐽 : ( ( On × On ) × 9o ) –1-1→ On
2		f1f	⊢ ( 𝐽 : ( ( On × On ) × 9o ) –1-1→ On → 𝐽 : ( ( On × On ) × 9o ) ⟶ On )
3		frn	⊢ ( 𝐽 : ( ( On × On ) × 9o ) ⟶ On → ran 𝐽 ⊆ On )
4	1 2 3	mp2b	⊢ ran 𝐽 ⊆ On
5		ssab	⊢ ( On ⊆ { 𝑤 ∣ ∃ 𝑧 ∈ ( ( On × On ) × 9o ) 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) } ↔ ∀ 𝑤 ( 𝑤 ∈ On → ∃ 𝑧 ∈ ( ( On × On ) × 9o ) 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) )
6		9on	⊢ 9o ∈ On
7		df-9o	⊢ 9o = suc 8o
8		nsuceq0	⊢ suc 8o ≠ ∅
9	7 8	eqnetri	⊢ 9o ≠ ∅
10		omeulem1	⊢ ( ( 9o ∈ On ∧ 𝑤 ∈ On ∧ 9o ≠ ∅ ) → ∃ 𝑡 ∈ On ∃ 𝑣 ∈ 9o ( ( 9o ·o 𝑡 ) +o 𝑣 ) = 𝑤 )
11	6 9 10	mp3an13	⊢ ( 𝑤 ∈ On → ∃ 𝑡 ∈ On ∃ 𝑣 ∈ 9o ( ( 9o ·o 𝑡 ) +o 𝑣 ) = 𝑤 )
12		j0iso	⊢ 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On )
13		isof1o	⊢ ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) → 𝐽0 : ( On × On ) –1-1-onto→ On )
14		f1ofo	⊢ ( 𝐽0 : ( On × On ) –1-1-onto→ On → 𝐽0 : ( On × On ) –onto→ On )
15	12 13 14	mp2b	⊢ 𝐽0 : ( On × On ) –onto→ On
16		foelcdmi	⊢ ( ( 𝐽0 : ( On × On ) –onto→ On ∧ 𝑡 ∈ On ) → ∃ 𝑢 ∈ ( On × On ) ( 𝐽0 ‘ 𝑢 ) = 𝑡 )
17	15 16	mpan	⊢ ( 𝑡 ∈ On → ∃ 𝑢 ∈ ( On × On ) ( 𝐽0 ‘ 𝑢 ) = 𝑡 )
18		oveq2	⊢ ( ( 𝐽0 ‘ 𝑢 ) = 𝑡 → ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) = ( 9o ·o 𝑡 ) )
19	18	oveq1d	⊢ ( ( 𝐽0 ‘ 𝑢 ) = 𝑡 → ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) = ( ( 9o ·o 𝑡 ) +o 𝑣 ) )
20	19	eqeq2d	⊢ ( ( 𝐽0 ‘ 𝑢 ) = 𝑡 → ( 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) ↔ 𝑤 = ( ( 9o ·o 𝑡 ) +o 𝑣 ) ) )
21		eqcom	⊢ ( 𝑤 = ( ( 9o ·o 𝑡 ) +o 𝑣 ) ↔ ( ( 9o ·o 𝑡 ) +o 𝑣 ) = 𝑤 )
22	20 21	bitrdi	⊢ ( ( 𝐽0 ‘ 𝑢 ) = 𝑡 → ( 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) ↔ ( ( 9o ·o 𝑡 ) +o 𝑣 ) = 𝑤 ) )
23	22	rexbidv	⊢ ( ( 𝐽0 ‘ 𝑢 ) = 𝑡 → ( ∃ 𝑣 ∈ 9o 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) ↔ ∃ 𝑣 ∈ 9o ( ( 9o ·o 𝑡 ) +o 𝑣 ) = 𝑤 ) )
24	23	biimprcd	⊢ ( ∃ 𝑣 ∈ 9o ( ( 9o ·o 𝑡 ) +o 𝑣 ) = 𝑤 → ( ( 𝐽0 ‘ 𝑢 ) = 𝑡 → ∃ 𝑣 ∈ 9o 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) ) )
25	24	reximdv	⊢ ( ∃ 𝑣 ∈ 9o ( ( 9o ·o 𝑡 ) +o 𝑣 ) = 𝑤 → ( ∃ 𝑢 ∈ ( On × On ) ( 𝐽0 ‘ 𝑢 ) = 𝑡 → ∃ 𝑢 ∈ ( On × On ) ∃ 𝑣 ∈ 9o 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) ) )
26	17 25	mpan9	⊢ ( ( 𝑡 ∈ On ∧ ∃ 𝑣 ∈ 9o ( ( 9o ·o 𝑡 ) +o 𝑣 ) = 𝑤 ) → ∃ 𝑢 ∈ ( On × On ) ∃ 𝑣 ∈ 9o 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) )
27	26	rexlimiva	⊢ ( ∃ 𝑡 ∈ On ∃ 𝑣 ∈ 9o ( ( 9o ·o 𝑡 ) +o 𝑣 ) = 𝑤 → ∃ 𝑢 ∈ ( On × On ) ∃ 𝑣 ∈ 9o 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) )
28	11 27	syl	⊢ ( 𝑤 ∈ On → ∃ 𝑢 ∈ ( On × On ) ∃ 𝑣 ∈ 9o 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) )
29		vex	⊢ 𝑢 ∈ V
30		vex	⊢ 𝑣 ∈ V
31	29 30	op1std	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 1st ‘ 𝑧 ) = 𝑢 )
32	31	fveq2d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) = ( 𝐽0 ‘ 𝑢 ) )
33	32	oveq2d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) = ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) )
34	29 30	op2ndd	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑣 )
35	33 34	oveq12d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) )
36	35	eqeq2d	⊢ ( 𝑧 = ⟨ 𝑢 , 𝑣 ⟩ → ( 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ↔ 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) ) )
37	36	rexxp	⊢ ( ∃ 𝑧 ∈ ( ( On × On ) × 9o ) 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ↔ ∃ 𝑢 ∈ ( On × On ) ∃ 𝑣 ∈ 9o 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ 𝑢 ) ) +o 𝑣 ) )
38	28 37	sylibr	⊢ ( 𝑤 ∈ On → ∃ 𝑧 ∈ ( ( On × On ) × 9o ) 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) )
39	5 38	mpgbir	⊢ On ⊆ { 𝑤 ∣ ∃ 𝑧 ∈ ( ( On × On ) × 9o ) 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) }
40		dfj2	⊢ 𝐽 = ( 𝑧 ∈ ( ( On × On ) × 9o ) ↦ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) )
41	40	rnmpt	⊢ ran 𝐽 = { 𝑤 ∣ ∃ 𝑧 ∈ ( ( On × On ) × 9o ) 𝑤 = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) }
42	39 41	sseqtrri	⊢ On ⊆ ran 𝐽
43	4 42	eqssi	⊢ ran 𝐽 = On
44		dff1o5	⊢ ( 𝐽 : ( ( On × On ) × 9o ) –1-1-onto→ On ↔ ( 𝐽 : ( ( On × On ) × 9o ) –1-1→ On ∧ ran 𝐽 = On ) )
45	1 43 44	mpbir2an	⊢ 𝐽 : ( ( On × On ) × 9o ) –1-1-onto→ On