Metamath Proof Explorer

Theorem jltalephlem

Description: Lemma for jltaleph . (Contributed by BTernaryTau, 16-Oct-2026)

Ref Expression
Assertion jltalephlem Could not format assertion : No typesetting found for |- ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 9on Could not format 9o e. On : No typesetting found for |- 9o e. On with typecode |-
2 j0iso Could not format _J0 Isom _R0 , _E ( ( On X. On ) , On ) : No typesetting found for |- _J0 Isom _R0 , _E ( ( On X. On ) , On ) with typecode |-
3 isof1o Could not format ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On ) : No typesetting found for |- ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) -> _J0 : ( On X. On ) -1-1-onto-> On ) with typecode |-
4 f1of Could not format ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On ) : No typesetting found for |- ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) --> On ) with typecode |-
5 2 3 4 mp2b Could not format _J0 : ( On X. On ) --> On : No typesetting found for |- _J0 : ( On X. On ) --> On with typecode |-
6 0elon ⊢ ∅ ∈ On
7 5 6 f0cli Could not format ( _J0 ` <. A , B >. ) e. On : No typesetting found for |- ( _J0 ` <. A , B >. ) e. On with typecode |-
8 omxpen Could not format ( ( 9o e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( 9o X. ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( 9o e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( 9o X. ( _J0 ` <. A , B >. ) ) ) with typecode |-
9 1 7 8 mp2an Could not format ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( 9o X. ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( 9o X. ( _J0 ` <. A , B >. ) ) with typecode |-
10 9onn Could not format 9o e. _om : No typesetting found for |- 9o e. _om with typecode |-
11 10 elexi Could not format 9o e. _V : No typesetting found for |- 9o e. _V with typecode |-
12 fvex Could not format ( _J0 ` <. A , B >. ) e. _V : No typesetting found for |- ( _J0 ` <. A , B >. ) e. _V with typecode |-
13 11 12 xpcomen Could not format ( 9o X. ( _J0 ` <. A , B >. ) ) ~~ ( ( _J0 ` <. A , B >. ) X. 9o ) : No typesetting found for |- ( 9o X. ( _J0 ` <. A , B >. ) ) ~~ ( ( _J0 ` <. A , B >. ) X. 9o ) with typecode |-
14 9 13 entri Could not format ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( ( _J0 ` <. A , B >. ) X. 9o ) : No typesetting found for |- ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( ( _J0 ` <. A , B >. ) X. 9o ) with typecode |-
15 nnfi Could not format ( 9o e. _om -> 9o e. Fin ) : No typesetting found for |- ( 9o e. _om -> 9o e. Fin ) with typecode |-
16 fict Could not format ( 9o e. Fin -> 9o ~<_ _om ) : No typesetting found for |- ( 9o e. Fin -> 9o ~<_ _om ) with typecode |-
17 10 15 16 mp2b Could not format 9o ~<_ _om : No typesetting found for |- 9o ~<_ _om with typecode |-
18 domtr Could not format ( ( 9o ~<_ _om /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> 9o ~<_ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( 9o ~<_ _om /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> 9o ~<_ ( _J0 ` <. A , B >. ) ) with typecode |-
19 17 18 mpan Could not format ( _om ~<_ ( _J0 ` <. A , B >. ) -> 9o ~<_ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( _om ~<_ ( _J0 ` <. A , B >. ) -> 9o ~<_ ( _J0 ` <. A , B >. ) ) with typecode |-
20 df-9o Could not format 9o = suc 8o : No typesetting found for |- 9o = suc 8o with typecode |-
21 nsuceq0 Could not format suc 8o =/= (/) : No typesetting found for |- suc 8o =/= (/) with typecode |-
22 20 21 eqnetri Could not format 9o =/= (/) : No typesetting found for |- 9o =/= (/) with typecode |-
23 onenon Could not format ( ( _J0 ` <. A , B >. ) e. On -> ( _J0 ` <. A , B >. ) e. dom card ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. On -> ( _J0 ` <. A , B >. ) e. dom card ) with typecode |-
24 7 23 ax-mp Could not format ( _J0 ` <. A , B >. ) e. dom card : No typesetting found for |- ( _J0 ` <. A , B >. ) e. dom card with typecode |-
25 infxpabs Could not format ( ( ( ( _J0 ` <. A , B >. ) e. dom card /\ _om ~<_ ( _J0 ` <. A , B >. ) ) /\ ( 9o =/= (/) /\ 9o ~<_ ( _J0 ` <. A , B >. ) ) ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( ( ( _J0 ` <. A , B >. ) e. dom card /\ _om ~<_ ( _J0 ` <. A , B >. ) ) /\ ( 9o =/= (/) /\ 9o ~<_ ( _J0 ` <. A , B >. ) ) ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
26 24 25 mpanl1 Could not format ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ ( 9o =/= (/) /\ 9o ~<_ ( _J0 ` <. A , B >. ) ) ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ ( 9o =/= (/) /\ 9o ~<_ ( _J0 ` <. A , B >. ) ) ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
27 22 26 mpanr1 Could not format ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ 9o ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ 9o ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
28 19 27 mpdan Could not format ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
29 entr Could not format ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( ( _J0 ` <. A , B >. ) X. 9o ) /\ ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( ( _J0 ` <. A , B >. ) X. 9o ) /\ ( ( _J0 ` <. A , B >. ) X. 9o ) ~~ ( _J0 ` <. A , B >. ) ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
30 14 28 29 sylancr Could not format ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( _om ~<_ ( _J0 ` <. A , B >. ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
31 ensym Could not format ( ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) -> ( _J0 ` <. A , B >. ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
32 domentr Could not format ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ ( _J0 ` <. A , B >. ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ ( _J0 ` <. A , B >. ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
33 31 32 sylan2 Could not format ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( _om ~<_ ( _J0 ` <. A , B >. ) /\ ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
34 30 33 mpdan Could not format ( _om ~<_ ( _J0 ` <. A , B >. ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( _om ~<_ ( _J0 ` <. A , B >. ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
35 omcl Could not format ( ( 9o e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. On ) : No typesetting found for |- ( ( 9o e. On /\ ( _J0 ` <. A , B >. ) e. On ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. On ) with typecode |-
36 1 7 35 mp2an Could not format ( 9o .o ( _J0 ` <. A , B >. ) ) e. On : No typesetting found for |- ( 9o .o ( _J0 ` <. A , B >. ) ) e. On with typecode |-
37 1 oneli Could not format ( C e. 9o -> C e. On ) : No typesetting found for |- ( C e. 9o -> C e. On ) with typecode |-
38 onadju Could not format ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. On /\ C e. On ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ) : No typesetting found for |- ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. On /\ C e. On ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ) with typecode |-
39 36 37 38 sylancr Could not format ( C e. 9o -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ) : No typesetting found for |- ( C e. 9o -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ) with typecode |-
40 onenon Could not format ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. On -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. dom card ) : No typesetting found for |- ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. On -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. dom card ) with typecode |-
41 36 40 ax-mp Could not format ( 9o .o ( _J0 ` <. A , B >. ) ) e. dom card : No typesetting found for |- ( 9o .o ( _J0 ` <. A , B >. ) ) e. dom card with typecode |-
42 simpr Could not format ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
43 elnn Could not format ( ( C e. 9o /\ 9o e. _om ) -> C e. _om ) : No typesetting found for |- ( ( C e. 9o /\ 9o e. _om ) -> C e. _om ) with typecode |-
44 10 43 mpan2 Could not format ( C e. 9o -> C e. _om ) : No typesetting found for |- ( C e. 9o -> C e. _om ) with typecode |-
45 nnfi ⊢ C ∈ ω → C ∈ Fin
46 fict ⊢ C ∈ Fin → C ≼ ω
47 44 45 46 3syl Could not format ( C e. 9o -> C ~<_ _om ) : No typesetting found for |- ( C e. 9o -> C ~<_ _om ) with typecode |-
48 domtr Could not format ( ( C ~<_ _om /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> C ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( C ~<_ _om /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> C ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
49 47 48 sylan Could not format ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> C ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> C ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
50 infdjuabs Could not format ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. dom card /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) /\ C ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. dom card /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) /\ C ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
51 41 42 49 50 mp3an2i Could not format ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
52 entr Could not format ( ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) /\ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) /\ ( ( 9o .o ( _J0 ` <. A , B >. ) ) |_| C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
53 39 51 52 syl2an2r Could not format ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( C e. 9o /\ _om ~<_ ( 9o .o ( _J0 ` <. A , B >. ) ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
54 34 53 sylan2 Could not format ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) ) with typecode |-
55 30 adantl Could not format ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
56 entr Could not format ( ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) /\ ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( 9o .o ( _J0 ` <. A , B >. ) ) /\ ( 9o .o ( _J0 ` <. A , B >. ) ) ~~ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
57 54 55 56 syl2anc Could not format ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( C e. 9o /\ _om ~<_ ( _J0 ` <. A , B >. ) ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-