Metamath Proof Explorer

Theorem jf1

Description: _J is a one-to-one function. Part of Proposition 15.3 of TakeutiZaring p. 155. (Contributed by BTernaryTau, 6-Oct-2026)

Ref Expression
Assertion jf1 𝐽 : ( ( On × On ) × 9o ) –1-1→ On

Proof

Step Hyp Ref Expression
1 9on ⊢ 9o ∈ On
2 j0iso ⊢ 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On )
3 isof1o ⊢ ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) → 𝐽0 : ( On × On ) –1-1-onto→ On )
4 2 3 ax-mp ⊢ 𝐽0 : ( On × On ) –1-1-onto→ On
5 f1of ⊢ ( 𝐽0 : ( On × On ) –1-1-onto→ On → 𝐽0 : ( On × On ) ⟶ On )
6 4 5 ax-mp ⊢ 𝐽0 : ( On × On ) ⟶ On
7 0elon ⊢ ∅ ∈ On
8 6 7 f0cli ⊢ ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ∈ On
9 omcl ⊢ ( ( 9o ∈ On ∧ ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ∈ On ) → ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) ∈ On )
10 1 8 9 mp2an ⊢ ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) ∈ On
11 xp2nd ⊢ ( 𝑤 ∈ ( ( On × On ) × 9o ) → ( 2nd ‘ 𝑤 ) ∈ 9o )
12 onelon ⊢ ( ( 9o ∈ On ∧ ( 2nd ‘ 𝑤 ) ∈ 9o ) → ( 2nd ‘ 𝑤 ) ∈ On )
13 1 11 12 sylancr ⊢ ( 𝑤 ∈ ( ( On × On ) × 9o ) → ( 2nd ‘ 𝑤 ) ∈ On )
14 oacl ⊢ ( ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) ∈ On ∧ ( 2nd ‘ 𝑤 ) ∈ On ) → ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) ∈ On )
15 10 13 14 sylancr ⊢ ( 𝑤 ∈ ( ( On × On ) × 9o ) → ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) ∈ On )
16 15 rgen ⊢ ∀ 𝑤 ∈ ( ( On × On ) × 9o ) ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) ∈ On
17 1 a1i ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → 9o ∈ On )
18 df-9o ⊢ 9o = suc 8o
19 nsuceq0 ⊢ suc 8o ≠ ∅
20 18 19 eqnetri ⊢ 9o ≠ ∅
21 20 a1i ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → 9o ≠ ∅ )
22 8 a1i ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ∈ On )
23 11 3ad2ant1 ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → ( 2nd ‘ 𝑤 ) ∈ 9o )
24 6 7 f0cli ⊢ ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ∈ On
25 24 a1i ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ∈ On )
26 xp2nd ⊢ ( 𝑧 ∈ ( ( On × On ) × 9o ) → ( 2nd ‘ 𝑧 ) ∈ 9o )
27 26 3ad2ant2 ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → ( 2nd ‘ 𝑧 ) ∈ 9o )
28 simp3 ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) )
29 17 21 22 23 25 27 28 omeueq ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → ( ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) = ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ∧ ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑧 ) ) )
30 xp1st ⊢ ( 𝑤 ∈ ( ( On × On ) × 9o ) → ( 1st ‘ 𝑤 ) ∈ ( On × On ) )
31 xp1st ⊢ ( 𝑧 ∈ ( ( On × On ) × 9o ) → ( 1st ‘ 𝑧 ) ∈ ( On × On ) )
32 f1of1 ⊢ ( 𝐽0 : ( On × On ) –1-1-onto→ On → 𝐽0 : ( On × On ) –1-1→ On )
33 4 32 ax-mp ⊢ 𝐽0 : ( On × On ) –1-1→ On
34 f1veqaeq ⊢ ( ( 𝐽0 : ( On × On ) –1-1→ On ∧ ( ( 1st ‘ 𝑤 ) ∈ ( On × On ) ∧ ( 1st ‘ 𝑧 ) ∈ ( On × On ) ) ) → ( ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) = ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) → ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑧 ) ) )
35 33 34 mpan ⊢ ( ( ( 1st ‘ 𝑤 ) ∈ ( On × On ) ∧ ( 1st ‘ 𝑧 ) ∈ ( On × On ) ) → ( ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) = ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) → ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑧 ) ) )
36 30 31 35 syl2an ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ) → ( ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) = ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) → ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑧 ) ) )
37 36 anim1d ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ) → ( ( ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) = ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ∧ ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑧 ) ) → ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑧 ) ∧ ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑧 ) ) ) )
38 37 3adant3 ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → ( ( ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) = ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ∧ ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑧 ) ) → ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑧 ) ∧ ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑧 ) ) ) )
39 29 38 mpd ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑧 ) ∧ ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑧 ) ) )
40 xpopth ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ) → ( ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑧 ) ∧ ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑧 ) ) ↔ 𝑤 = 𝑧 ) )
41 40 3adant3 ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → ( ( ( 1st ‘ 𝑤 ) = ( 1st ‘ 𝑧 ) ∧ ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑧 ) ) ↔ 𝑤 = 𝑧 ) )
42 39 41 mpbid ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ∧ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) ) → 𝑤 = 𝑧 )
43 42 3expia ⊢ ( ( 𝑤 ∈ ( ( On × On ) × 9o ) ∧ 𝑧 ∈ ( ( On × On ) × 9o ) ) → ( ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) → 𝑤 = 𝑧 ) )
44 43 rgen2 ⊢ ∀ 𝑤 ∈ ( ( On × On ) × 9o ) ∀ 𝑧 ∈ ( ( On × On ) × 9o ) ( ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) → 𝑤 = 𝑧 )
45 dfj2 ⊢ 𝐽 = ( 𝑤 ∈ ( ( On × On ) × 9o ) ↦ ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) )
46 2fveq3 ⊢ ( 𝑤 = 𝑧 → ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) = ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) )
47 46 oveq2d ⊢ ( 𝑤 = 𝑧 → ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) = ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) )
48 fveq2 ⊢ ( 𝑤 = 𝑧 → ( 2nd ‘ 𝑤 ) = ( 2nd ‘ 𝑧 ) )
49 47 48 oveq12d ⊢ ( 𝑤 = 𝑧 → ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) )
50 45 49 f1mpt ⊢ ( 𝐽 : ( ( On × On ) × 9o ) –1-1→ On ↔ ( ∀ 𝑤 ∈ ( ( On × On ) × 9o ) ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) ∈ On ∧ ∀ 𝑤 ∈ ( ( On × On ) × 9o ) ∀ 𝑧 ∈ ( ( On × On ) × 9o ) ( ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑤 ) ) ) +o ( 2nd ‘ 𝑤 ) ) = ( ( 9o ·o ( 𝐽0 ‘ ( 1st ‘ 𝑧 ) ) ) +o ( 2nd ‘ 𝑧 ) ) → 𝑤 = 𝑧 ) ) )
51 16 44 50 mpbir2an ⊢ 𝐽 : ( ( On × On ) × 9o ) –1-1→ On