Metamath Proof Explorer

Theorem jltaleph

Description: The value of _J is less than an aleph if its first two arguments are less than that aleph. Proposition 15.11 of TakeutiZaring p. 156. (Contributed by BTernaryTau, 16-Oct-2026)

Ref Expression
Assertion jltaleph ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) )

Proof

Step Hyp Ref Expression
1 alephon ⊢ ( ℵ ‘ 𝐷 ) ∈ On
2 1 oneli ⊢ ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) → 𝐴 ∈ On )
3 2 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → 𝐴 ∈ On )
4 1 oneli ⊢ ( 𝐵 ∈ ( ℵ ‘ 𝐷 ) → 𝐵 ∈ On )
5 4 3ad2ant2 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → 𝐵 ∈ On )
6 simp3 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → 𝐶 ∈ 9o )
7 ovexd ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ∈ V )
8 opeq1 ⊢ ( 𝐴 = 𝑥 → ⟨ 𝐴 , 𝑦 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ )
9 8 fveq2d ⊢ ( 𝐴 = 𝑥 → ( 𝐽0 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) = ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
10 9 oveq2d ⊢ ( 𝐴 = 𝑥 → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) = ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) )
11 10 oveq1d ⊢ ( 𝐴 = 𝑥 → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) +o 𝑛 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 ) )
12 11 adantl ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ 𝐴 = 𝑥 ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) +o 𝑛 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 ) )
13 opeq2 ⊢ ( 𝐵 = 𝑦 → ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝐴 , 𝑦 ⟩ )
14 13 fveq2d ⊢ ( 𝐵 = 𝑦 → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( 𝐽0 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) )
15 14 oveq2d ⊢ ( 𝐵 = 𝑦 → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) )
16 15 oveq1d ⊢ ( 𝐵 = 𝑦 → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝑛 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) +o 𝑛 ) )
17 16 adantl ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ 𝐵 = 𝑦 ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝑛 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝑦 ⟩ ) ) +o 𝑛 ) )
18 oveq2 ⊢ ( 𝐶 = 𝑛 → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝑛 ) )
19 18 adantl ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ 𝐶 = 𝑛 ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝑛 ) )
20 df-j ⊢ 𝐽 = ( 𝑥 ∈ On , 𝑦 ∈ On , 𝑛 ∈ 9o ↦ ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ) +o 𝑛 ) )
21 3 5 6 7 12 17 19 20 mpt3fvot2d ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) )
22 21 adantr ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) )
23 6 anim1ci ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ∧ 𝐶 ∈ 9o ) )
24 alephfnon ⊢ ℵ Fn On
25 24 fndmi ⊢ dom ℵ = On
26 25 eleq2i ⊢ ( 𝐷 ∈ dom ℵ ↔ 𝐷 ∈ On )
27 ndmfv ⊢ ( ¬ 𝐷 ∈ dom ℵ → ( ℵ ‘ 𝐷 ) = ∅ )
28 26 27 sylnbir ⊢ ( ¬ 𝐷 ∈ On → ( ℵ ‘ 𝐷 ) = ∅ )
29 nel02 ⊢ ( ( ℵ ‘ 𝐷 ) = ∅ → ¬ 𝐴 ∈ ( ℵ ‘ 𝐷 ) )
30 28 29 syl ⊢ ( ¬ 𝐷 ∈ On → ¬ 𝐴 ∈ ( ℵ ‘ 𝐷 ) )
31 30 con4i ⊢ ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) → 𝐷 ∈ On )
32 31 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → 𝐷 ∈ On )
33 32 adantr ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → 𝐷 ∈ On )
34 alephgeom ⊢ ( 𝐷 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐷 ) )
35 34 bilani ⊢ ( ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ∧ 𝐶 ∈ 9o ) ∧ 𝐷 ∈ On ) → ω ⊆ ( ℵ ‘ 𝐷 ) )
36 9onn ⊢ 9o ∈ ω
37 nnmcl ⊢ ( ( 9o ∈ ω ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ ω )
38 36 37 mpan ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω → ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ ω )
39 elnn ⊢ ( ( 𝐶 ∈ 9o ∧ 9o ∈ ω ) → 𝐶 ∈ ω )
40 36 39 mpan2 ⊢ ( 𝐶 ∈ 9o → 𝐶 ∈ ω )
41 nnacl ⊢ ( ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) ∈ ω ∧ 𝐶 ∈ ω ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ∈ ω )
42 38 40 41 syl2an ⊢ ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ∧ 𝐶 ∈ 9o ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ∈ ω )
43 42 adantr ⊢ ( ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ∧ 𝐶 ∈ 9o ) ∧ 𝐷 ∈ On ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ∈ ω )
44 35 43 sseldd ⊢ ( ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ∧ 𝐶 ∈ 9o ) ∧ 𝐷 ∈ On ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ∈ ( ℵ ‘ 𝐷 ) )
45 23 33 44 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ∈ ( ℵ ‘ 𝐷 ) )
46 22 45 eqeltrd ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) )
47 21 adantr ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) = ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) )
48 j0iso ⊢ 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On )
49 isof1o ⊢ ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) → 𝐽0 : ( On × On ) –1-1-onto→ On )
50 f1of ⊢ ( 𝐽0 : ( On × On ) –1-1-onto→ On → 𝐽0 : ( On × On ) ⟶ On )
51 48 49 50 mp2b ⊢ 𝐽0 : ( On × On ) ⟶ On
52 0elon ⊢ ∅ ∈ On
53 51 52 f0cli ⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On
54 onfin ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin ↔ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) )
55 54 notbid ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On → ( ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin ↔ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) )
56 onenon ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ dom card )
57 infinfnum ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ dom card → ( ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin ↔ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
58 56 57 syl ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On → ( ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin ↔ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
59 55 58 bitr3d ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On → ( ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ↔ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
60 53 59 ax-mp ⊢ ( ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ↔ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
61 jltalephlem ⊢ ( ( 𝐶 ∈ 9o ∧ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
62 60 61 sylan2b ⊢ ( ( 𝐶 ∈ 9o ∧ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
63 62 3ad2antl3 ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( ( 9o ·o ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) +o 𝐶 ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
64 47 63 eqbrtrd ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
65 j0ltaleph ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) )
66 alephsdom ⊢ ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On ∧ 𝐷 ∈ On ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) ↔ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) ) )
67 53 31 66 sylancr ⊢ ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) ↔ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) ) )
68 67 adantr ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) ↔ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) ) )
69 65 68 mpbid ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) )
70 69 3adant3 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) )
71 70 adantr ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) )
72 ensdomtr ⊢ ( ( ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ≈ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) )
73 64 71 72 syl2anc ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) )
74 jf1 ⊢ 𝐽 : ( ( On × On ) × 9o ) –1-1→ On
75 f1f ⊢ ( 𝐽 : ( ( On × On ) × 9o ) –1-1→ On → 𝐽 : ( ( On × On ) × 9o ) ⟶ On )
76 74 75 ax-mp ⊢ 𝐽 : ( ( On × On ) × 9o ) ⟶ On
77 76 52 f0cli ⊢ ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ On
78 alephsdom ⊢ ( ( ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ On ∧ 𝐷 ∈ On ) → ( ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) ↔ ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) ) )
79 77 31 78 sylancr ⊢ ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) → ( ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) ↔ ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) ) )
80 79 3ad2ant1 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → ( ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) ↔ ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) ) )
81 80 adantr ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) ↔ ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ≺ ( ℵ ‘ 𝐷 ) ) )
82 73 81 mpbird ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) ∧ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) )
83 46 82 pm2.61dan ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐷 ) ∧ 𝐶 ∈ 9o ) → ( 𝐽 ‘ ⟨ 𝐴 , 𝐵 , 𝐶 ⟩ ) ∈ ( ℵ ‘ 𝐷 ) )