Metamath Proof Explorer

Theorem j0ltalephlem

Description: Lemma for j0ltaleph . (Contributed by BTernaryTau, 25-Sep-2026)

Ref Expression
Assertion j0ltalephlem ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 fvex ⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V
2 j0iso ⊢ 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On )
3 opelxpi ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) )
4 imassrn ⊢ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ⊆ ran ◡ 𝑅0
5 dfdm4 ⊢ dom 𝑅0 = ran ◡ 𝑅0
6 dmr0ss ⊢ dom 𝑅0 ⊆ ( On × On )
7 5 6 eqsstrri ⊢ ran ◡ 𝑅0 ⊆ ( On × On )
8 4 7 sstri ⊢ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ⊆ ( On × On )
9 sseqin2 ⊢ ( ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ⊆ ( On × On ) ↔ ( ( On × On ) ∩ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) = ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
10 8 9 mpbi ⊢ ( ( On × On ) ∩ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) = ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } )
11 10 eqcomi ⊢ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) = ( ( On × On ) ∩ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
12 1 epini ⊢ ( ◡ E “ { ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) } ) = ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
13 12 ineq2i ⊢ ( On ∩ ( ◡ E “ { ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) } ) ) = ( On ∩ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
14 isof1o ⊢ ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) → 𝐽0 : ( On × On ) –1-1-onto→ On )
15 f1of ⊢ ( 𝐽0 : ( On × On ) –1-1-onto→ On → 𝐽0 : ( On × On ) ⟶ On )
16 2 14 15 mp2b ⊢ 𝐽0 : ( On × On ) ⟶ On
17 0elon ⊢ ∅ ∈ On
18 16 17 f0cli ⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ On
19 18 onssi ⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⊆ On
20 sseqin2 ⊢ ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ⊆ On ↔ ( On ∩ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
21 19 20 mpbi ⊢ ( On ∩ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) = ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ )
22 13 21 eqtr2i ⊢ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( On ∩ ( ◡ E “ { ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) } ) )
23 11 22 isoini2 ⊢ ( ( 𝐽0 Isom 𝑅0 , E ( ( On × On ) , On ) ∧ ⟨ 𝐴 , 𝐵 ⟩ ∈ ( On × On ) ) → ( 𝐽0 ↾ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) Isom 𝑅0 , E ( ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) , ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
24 2 3 23 sylancr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐽0 ↾ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) Isom 𝑅0 , E ( ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) , ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) )
25 isof1o ⊢ ( ( 𝐽0 ↾ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) Isom 𝑅0 , E ( ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) , ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ) → ( 𝐽0 ↾ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) : ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) –1-1-onto→ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
26 f1ocnv ⊢ ( ( 𝐽0 ↾ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) : ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) –1-1-onto→ ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) → ◡ ( 𝐽0 ↾ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) : ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) –1-1-onto→ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
27 24 25 26 3syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ◡ ( 𝐽0 ↾ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) : ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) –1-1-onto→ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
28 f1oeng ⊢ ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ V ∧ ◡ ( 𝐽0 ↾ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) : ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) –1-1-onto→ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
29 1 27 28 sylancr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) )
30 onun2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ∈ On )
31 onsuc ⊢ ( ( 𝐴 ∪ 𝐵 ) ∈ On → suc ( 𝐴 ∪ 𝐵 ) ∈ On )
32 30 31 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → suc ( 𝐴 ∪ 𝐵 ) ∈ On )
33 32 32 xpexd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ∈ V )
34 simplrl ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → 𝑥 ∈ On )
35 simplrr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → 𝑦 ∈ On )
36 simplll ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → 𝐴 ∈ On )
37 simpllr ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → 𝐵 ∈ On )
38 opex ⊢ ⟨ 𝐴 , 𝐵 ⟩ ∈ V
39 opex ⊢ ⟨ 𝑥 , 𝑦 ⟩ ∈ V
40 39 eliniseg ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ ∈ V → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ ) )
41 38 40 ax-mp ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ )
42 41 bilani ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ⟨ 𝑥 , 𝑦 ⟩ 𝑅0 ⟨ 𝐴 , 𝐵 ⟩ )
43 34 35 36 37 42 r0maxss ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝑥 ∪ 𝑦 ) ⊆ ( 𝐴 ∪ 𝐵 ) )
44 43 unssad ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → 𝑥 ⊆ ( 𝐴 ∪ 𝐵 ) )
45 36 37 30 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝐴 ∪ 𝐵 ) ∈ On )
46 onsssuc ⊢ ( ( 𝑥 ∈ On ∧ ( 𝐴 ∪ 𝐵 ) ∈ On ) → ( 𝑥 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) ) )
47 34 45 46 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝑥 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) ) )
48 44 47 mpbid ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → 𝑥 ∈ suc ( 𝐴 ∪ 𝐵 ) )
49 43 unssbd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → 𝑦 ⊆ ( 𝐴 ∪ 𝐵 ) )
50 onsssuc ⊢ ( ( 𝑦 ∈ On ∧ ( 𝐴 ∪ 𝐵 ) ∈ On ) → ( 𝑦 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ 𝑦 ∈ suc ( 𝐴 ∪ 𝐵 ) ) )
51 35 45 50 syl2anc ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ( 𝑦 ⊆ ( 𝐴 ∪ 𝐵 ) ↔ 𝑦 ∈ suc ( 𝐴 ∪ 𝐵 ) ) )
52 49 51 mpbid ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → 𝑦 ∈ suc ( 𝐴 ∪ 𝐵 ) )
53 48 52 opelxpd ⊢ ( ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) )
54 53 ex ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑥 ∈ On ∧ 𝑦 ∈ On ) ) → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ) )
55 54 ralrimivva ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ) )
56 ssrel2 ⊢ ( ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ⊆ ( On × On ) → ( ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ⊆ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ↔ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ) ) )
57 8 56 ax-mp ⊢ ( ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ⊆ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ↔ ∀ 𝑥 ∈ On ∀ 𝑦 ∈ On ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) → ⟨ 𝑥 , 𝑦 ⟩ ∈ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ) )
58 55 57 sylibr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ⊆ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) )
59 ssdomg ⊢ ( ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ∈ V → ( ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ⊆ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) → ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ) )
60 33 58 59 sylc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) )
61 endomtr ⊢ ( ( ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≈ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ∧ ( ◡ 𝑅0 “ { ⟨ 𝐴 , 𝐵 ⟩ } ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) )
62 29 60 61 syl2anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐽0 ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ≼ ( suc ( 𝐴 ∪ 𝐵 ) × suc ( 𝐴 ∪ 𝐵 ) ) )