Metamath Proof Explorer

Theorem j0ltaleph

Description: The value of _J0 is less than an aleph if its two arguments are less than that aleph. Proposition 15.1(2) of TakeutiZaring p. 154. (Contributed by BTernaryTau, 25-Sep-2026)

Ref Expression
Assertion j0ltaleph ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) )

Proof

Step Hyp Ref Expression
1 omelon ⊢ ω ∈ 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 f1of ⊢ ( 𝐽0 : ( On × On ) –1-1-onto→ On → 𝐽0 : ( On × On ) ⟶ On )
5 2 3 4 mp2b ⊢ 𝐽0 : ( On × On ) ⟶ On
6 0elon ⊢ ∅ ∈ On
7 5 6 f0cli ⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On
8 domtriord ⊢ ( ( ω ∈ On ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On ) → ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ω ) )
9 1 7 8 mp2an ⊢ ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ↔ ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ω )
10 9 con2bii ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ω ↔ ¬ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
11 sdomel ⊢ ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On ∧ ω ∈ On ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ω → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) )
12 7 1 11 mp2an ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ω → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω )
13 10 12 sylbir ⊢ ( ¬ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω )
14 13 orri ⊢ ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∨ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω )
15 alephon ⊢ ( ℵ ‘ 𝐶 ) ∈ On
16 15 oneli ⊢ ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) → 𝐴 ∈ On )
17 15 oneli ⊢ ( 𝐵 ∈ ( ℵ ‘ 𝐶 ) → 𝐵 ∈ On )
18 16 17 anim12i ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) → ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) )
19 18 3adant3 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) )
20 j0ltalephlem ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) )
21 xpfi ⊢ ( ( suc ( 𝐴 ∪ 𝐵 ) ∈ Fin ∧ suc ( 𝐴 ∪ 𝐵 ) ∈ Fin ) → ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ∈ Fin )
22 21 anidms ⊢ ( suc ( 𝐴 ∪ 𝐵 ) ∈ Fin → ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ∈ Fin )
23 domfi ⊢ ( ( ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ∈ Fin ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin )
24 22 23 sylan ⊢ ( ( suc ( 𝐴 ∪ 𝐵 ) ∈ Fin ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin )
25 24 expcom ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) → ( suc ( 𝐴 ∪ 𝐵 ) ∈ Fin → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin ) )
26 20 25 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( suc ( 𝐴 ∪ 𝐵 ) ∈ Fin → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin ) )
27 onenon ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ dom card )
28 infinfnum ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ dom card → ( ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin ↔ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
29 7 27 28 mp2b ⊢ ( ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin ↔ ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
30 29 biimpri ⊢ ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ¬ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ Fin )
31 26 30 nsyli ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ¬ suc ( 𝐴 ∪ 𝐵 ) ∈ Fin ) )
32 onun2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ∈ On )
33 onsuc ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ On → suc ( 𝐴 ∪ 𝐵 ) ∈ On )
34 onenon ⊢ ( suc ( 𝐴 ∪ 𝐵 ) ∈ On → suc ( 𝐴 ∪ 𝐵 ) ∈ dom card )
35 32 33 34 3syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ( 𝐴 ∪ 𝐵 ) ∈ dom card )
36 infinfnum ⊢ ( suc ( 𝐴 ∪ 𝐵 ) ∈ dom card → ( ¬ suc ( 𝐴 ∪ 𝐵 ) ∈ Fin ↔ ω ≼ suc ( 𝐴 ∪ 𝐵 ) ) )
37 35 36 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ¬ suc ( 𝐴 ∪ 𝐵 ) ∈ Fin ↔ ω ≼ suc ( 𝐴 ∪ 𝐵 ) ) )
38 31 37 sylibd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ω ≼ suc ( 𝐴 ∪ 𝐵 ) ) )
39 19 38 syl ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ω ≼ suc ( 𝐴 ∪ 𝐵 ) ) )
40 infxpidm2 ⊢ ( ( suc ( 𝐴 ∪ 𝐵 ) ∈ dom card ∧ ω ≼ suc ( 𝐴 ∪ 𝐵 ) ) → ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ≈ suc ( 𝐴 ∪ 𝐵 ) )
41 35 40 sylan ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ω ≼ suc ( 𝐴 ∪ 𝐵 ) ) → ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ≈ suc ( 𝐴 ∪ 𝐵 ) )
42 41 ex ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ω ≼ suc ( 𝐴 ∪ 𝐵 ) → ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ≈ suc ( 𝐴 ∪ 𝐵 ) ) )
43 domentr ⊢ ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ∧ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ≈ suc ( 𝐴 ∪ 𝐵 ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ suc ( 𝐴 ∪ 𝐵 ) )
44 20 42 43 syl6an ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ω ≼ suc ( 𝐴 ∪ 𝐵 ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ suc ( 𝐴 ∪ 𝐵 ) ) )
45 19 44 syl ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ω ≼ suc ( 𝐴 ∪ 𝐵 ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ suc ( 𝐴 ∪ 𝐵 ) ) )
46 onunel ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ ( ℵ ‘ 𝐶 ) ∈ On ) → ( ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ↔ ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) ) )
47 15 46 mp3an3 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ↔ ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) ) )
48 16 17 47 syl2an ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) → ( ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ↔ ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) ) )
49 48 ibir ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) → ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) )
50 49 3adant3 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) )
51 alephislim ⊢ ( 𝐶 ∈ On ↔ Lim ( ℵ ‘ 𝐶 ) )
52 limsuc ⊢ ( Lim ( ℵ ‘ 𝐶 ) → ( ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ↔ suc ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ) )
53 51 52 sylbi ⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ↔ suc ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ) )
54 53 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ↔ suc ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ) )
55 50 54 mpbid ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → suc ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) )
56 18 32 33 3syl ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) → suc ( 𝐴 ∪ 𝐵 ) ∈ On )
57 alephsdom ⊢ ( ( suc ( 𝐴 ∪ 𝐵 ) ∈ On ∧ 𝐶 ∈ On ) → ( suc ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ↔ suc ( 𝐴 ∪ 𝐵 ) ≺ ( ℵ ‘ 𝐶 ) ) )
58 56 57 stoic3 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( suc ( 𝐴 ∪ 𝐵 ) ∈ ( ℵ ‘ 𝐶 ) ↔ suc ( 𝐴 ∪ 𝐵 ) ≺ ( ℵ ‘ 𝐶 ) ) )
59 55 58 mpbid ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → suc ( 𝐴 ∪ 𝐵 ) ≺ ( ℵ ‘ 𝐶 ) )
60 45 59 jctird ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ω ≼ suc ( 𝐴 ∪ 𝐵 ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ suc ( 𝐴 ∪ 𝐵 ) ∧ suc ( 𝐴 ∪ 𝐵 ) ≺ ( ℵ ‘ 𝐶 ) ) ) )
61 domsdomtr ⊢ ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ suc ( 𝐴 ∪ 𝐵 ) ∧ suc ( 𝐴 ∪ 𝐵 ) ≺ ( ℵ ‘ 𝐶 ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐶 ) )
62 60 61 syl6 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ω ≼ suc ( 𝐴 ∪ 𝐵 ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐶 ) ) )
63 39 62 syld ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐶 ) ) )
64 alephsdom ⊢ ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On ∧ 𝐶 ∈ On ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) ↔ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐶 ) ) )
65 7 64 mpan ⊢ ( 𝐶 ∈ On → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) ↔ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐶 ) ) )
66 65 3ad2ant3 ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) ↔ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≺ ( ℵ ‘ 𝐶 ) ) )
67 63 66 sylibrd ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) ) )
68 alephgeom ⊢ ( 𝐶 ∈ On ↔ ω ⊆ ( ℵ ‘ 𝐶 ) )
69 68 biimpi ⊢ ( 𝐶 ∈ On → ω ⊆ ( ℵ ‘ 𝐶 ) )
70 69 sselda ⊢ ( ( 𝐶 ∈ On ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) )
71 70 3ad2antl3 ⊢ ( ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) ∧ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) )
72 71 ex ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) ) )
73 67 72 jaod ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( ( ω ≼ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∨ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ω ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) ) )
74 14 73 mpi ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐶 ∈ On ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) )
75 74 3expia ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) → ( 𝐶 ∈ On → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) ) )
76 75 com12 ⊢ ( 𝐶 ∈ On → ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) ) )
77 alephfnon ⊢ ℵ Fn On
78 77 fndmi ⊢ dom ℵ = On
79 78 eleq2i ⊢ ( 𝐶 ∈ dom ℵ ↔ 𝐶 ∈ On )
80 ndmfv ⊢ ( ¬ 𝐶 ∈ dom ℵ → ( ℵ ‘ 𝐶 ) = ∅ )
81 79 80 sylnbir ⊢ ( ¬ 𝐶 ∈ On → ( ℵ ‘ 𝐶 ) = ∅ )
82 nel02 ⊢ ( ( ℵ ‘ 𝐶 ) = ∅ → ¬ 𝐴 ∈ ( ℵ ‘ 𝐶 ) )
83 81 82 syl ⊢ ( ¬ 𝐶 ∈ On → ¬ 𝐴 ∈ ( ℵ ‘ 𝐶 ) )
84 83 intnanrd ⊢ ( ¬ 𝐶 ∈ On → ¬ ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) )
85 84 pm2.21d ⊢ ( ¬ 𝐶 ∈ On → ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) ) )
86 76 85 pm2.61i ⊢ ( ( 𝐴 ∈ ( ℵ ‘ 𝐶 ) ∧ 𝐵 ∈ ( ℵ ‘ 𝐶 ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( ℵ ‘ 𝐶 ) )