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	Could not format assertion : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		alephon	$$⊢\aleph \left(D\right)\in \mathrm{On}$$
2	1	oneli	$$⊢A\in \aleph \left(D\right)\to A\in \mathrm{On}$$
3	2	3ad2ant1	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> A e. On ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> A e. On ) with typecode |-
4	1	oneli	$$⊢B\in \aleph \left(D\right)\to B\in \mathrm{On}$$
5	4	3ad2ant2	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> B e. On ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> B e. On ) with typecode |-
6		simp3	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> C e. 9o ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> C e. 9o ) with typecode |-
7		ovexd	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _V ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _V ) with typecode |-
8		opeq1	$$⊢A=x\to ⟨A,y⟩=⟨x,y⟩$$
9	8	fveq2d	Could not format ( A = x -> ( _J0 ` <. A , y >. ) = ( _J0 ` <. x , y >. ) ) : No typesetting found for |- ( A = x -> ( _J0 ` <. A , y >. ) = ( _J0 ` <. x , y >. ) ) with typecode |-
10	9	oveq2d	Could not format ( A = x -> ( 9o .o ( _J0 ` <. A , y >. ) ) = ( 9o .o ( _J0 ` <. x , y >. ) ) ) : No typesetting found for |- ( A = x -> ( 9o .o ( _J0 ` <. A , y >. ) ) = ( 9o .o ( _J0 ` <. x , y >. ) ) ) with typecode |-
11	10	oveq1d	Could not format ( A = x -> ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) : No typesetting found for |- ( A = x -> ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) with typecode |-
12	11	adantl	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ A = x ) -> ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ A = x ) -> ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) with typecode |-
13		opeq2	$$⊢B=y\to ⟨A,B⟩=⟨A,y⟩$$
14	13	fveq2d	Could not format ( B = y -> ( _J0 ` <. A , B >. ) = ( _J0 ` <. A , y >. ) ) : No typesetting found for |- ( B = y -> ( _J0 ` <. A , B >. ) = ( _J0 ` <. A , y >. ) ) with typecode |-
15	14	oveq2d	Could not format ( B = y -> ( 9o .o ( _J0 ` <. A , B >. ) ) = ( 9o .o ( _J0 ` <. A , y >. ) ) ) : No typesetting found for |- ( B = y -> ( 9o .o ( _J0 ` <. A , B >. ) ) = ( 9o .o ( _J0 ` <. A , y >. ) ) ) with typecode |-
16	15	oveq1d	Could not format ( B = y -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) ) : No typesetting found for |- ( B = y -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) ) with typecode |-
17	16	adantl	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ B = y ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ B = y ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) = ( ( 9o .o ( _J0 ` <. A , y >. ) ) +o n ) ) with typecode |-
18		oveq2	Could not format ( C = n -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) ) : No typesetting found for |- ( C = n -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) ) with typecode |-
19	18	adantl	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ C = n ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ C = n ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o n ) ) with typecode |-
20		df-j	Could not format _J = ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) : No typesetting found for |- _J = ( x e. On , y e. On , n e. 9o |-> ( ( 9o .o ( _J0 ` <. x , y >. ) ) +o n ) ) with typecode |-
21	3 5 6 7 12 17 19 20	mpt3fvot2d	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J ` <. A , B , C >. ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J ` <. A , B , C >. ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ) with typecode |-
22	21	adantr	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ) with typecode |-
23	6	anim1ci	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) ) with typecode |-
24		alephfnon	$$⊢\aleph Fn\mathrm{On}$$
25	24	fndmi	$$⊢\mathrm{dom}\aleph =\mathrm{On}$$
26	25	eleq2i	$$⊢D\in \mathrm{dom}\aleph \leftrightarrow D\in \mathrm{On}$$
27		ndmfv	$$⊢\neg D\in \mathrm{dom}\aleph \to \aleph \left(D\right)=\varnothing$$
28	26 27	sylnbir	$$⊢\neg D\in \mathrm{On}\to \aleph \left(D\right)=\varnothing$$
29		nel02	$$⊢\aleph \left(D\right)=\varnothing \to \neg A\in \aleph \left(D\right)$$
30	28 29	syl	$$⊢\neg D\in \mathrm{On}\to \neg A\in \aleph \left(D\right)$$
31	30	con4i	$$⊢A\in \aleph \left(D\right)\to D\in \mathrm{On}$$
32	31	3ad2ant1	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> D e. On ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> D e. On ) with typecode |-
33	32	adantr	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> D e. On ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> D e. On ) with typecode |-
34		alephgeom	$$⊢D\in \mathrm{On}\leftrightarrow \mathrm{\omega }\subseteq \aleph \left(D\right)$$
35	34	bilani	Could not format ( ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) /\ D e. On ) -> _om C_ ( aleph ` D ) ) : No typesetting found for |- ( ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) /\ D e. On ) -> _om C_ ( aleph ` D ) ) with typecode |-
36		9onn	Could not format 9o e. _om : No typesetting found for |- 9o e. _om with typecode |-
37		nnmcl	Could not format ( ( 9o e. _om /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. _om ) : No typesetting found for |- ( ( 9o e. _om /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. _om ) with typecode |-
38	36 37	mpan	Could not format ( ( _J0 ` <. A , B >. ) e. _om -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. _om ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. _om -> ( 9o .o ( _J0 ` <. A , B >. ) ) e. _om ) with typecode |-
39		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 |-
40	36 39	mpan2	Could not format ( C e. 9o -> C e. _om ) : No typesetting found for |- ( C e. 9o -> C e. _om ) with typecode |-
41		nnacl	Could not format ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. _om /\ C e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _om ) : No typesetting found for |- ( ( ( 9o .o ( _J0 ` <. A , B >. ) ) e. _om /\ C e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _om ) with typecode |-
42	38 40 41	syl2an	Could not format ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _om ) : No typesetting found for |- ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _om ) with typecode |-
43	42	adantr	Could not format ( ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) /\ D e. On ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _om ) : No typesetting found for |- ( ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) /\ D e. On ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. _om ) with typecode |-
44	35 43	sseldd	Could not format ( ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) /\ D e. On ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. ( aleph ` D ) ) : No typesetting found for |- ( ( ( ( _J0 ` <. A , B >. ) e. _om /\ C e. 9o ) /\ D e. On ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. ( aleph ` D ) ) with typecode |-
45	23 33 44	syl2anc	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. ( aleph ` D ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) e. ( aleph ` D ) ) with typecode |-
46	22 45	eqeltrd	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) ) with typecode |-
47	21	adantr	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) = ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ) with typecode |-
48		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 |-
49		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 |-
50		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 |-
51	48 49 50	mp2b	Could not format _J0 : ( On X. On ) --> On : No typesetting found for |- _J0 : ( On X. On ) --> On with typecode |-
52		0elon	$$⊢\varnothing \in \mathrm{On}$$
53	51 52	f0cli	Could not format ( _J0 ` <. A , B >. ) e. On : No typesetting found for |- ( _J0 ` <. A , B >. ) e. On with typecode |-
54		onfin	Could not format ( ( _J0 ` <. A , B >. ) e. On -> ( ( _J0 ` <. A , B >. ) e. Fin <-> ( _J0 ` <. A , B >. ) e. _om ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. On -> ( ( _J0 ` <. A , B >. ) e. Fin <-> ( _J0 ` <. A , B >. ) e. _om ) ) with typecode |-
55	54	notbid	Could not format ( ( _J0 ` <. A , B >. ) e. On -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> -. ( _J0 ` <. A , B >. ) e. _om ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. On -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> -. ( _J0 ` <. A , B >. ) e. _om ) ) with typecode |-
56		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 |-
57		infinfnum	Could not format ( ( _J0 ` <. A , B >. ) e. dom card -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. dom card -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) ) with typecode |-
58	56 57	syl	Could not format ( ( _J0 ` <. A , B >. ) e. On -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. On -> ( -. ( _J0 ` <. A , B >. ) e. Fin <-> _om ~<_ ( _J0 ` <. A , B >. ) ) ) with typecode |-
59	55 58	bitr3d	Could not format ( ( _J0 ` <. A , B >. ) e. On -> ( -. ( _J0 ` <. A , B >. ) e. _om <-> _om ~<_ ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) e. On -> ( -. ( _J0 ` <. A , B >. ) e. _om <-> _om ~<_ ( _J0 ` <. A , B >. ) ) ) with typecode |-
60	53 59	ax-mp	Could not format ( -. ( _J0 ` <. A , B >. ) e. _om <-> _om ~<_ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( -. ( _J0 ` <. A , B >. ) e. _om <-> _om ~<_ ( _J0 ` <. A , B >. ) ) with typecode |-
61		jltalephlem	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 |-
62	60 61	sylan2b	Could not format ( ( C e. 9o /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( C e. 9o /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
63	62	3ad2antl3	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( ( 9o .o ( _J0 ` <. A , B >. ) ) +o C ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
64	47 63	eqbrtrd	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) ~~ ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) ~~ ( _J0 ` <. A , B >. ) ) with typecode |-
65		j0ltaleph	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` D ) ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) ) -> ( _J0 ` <. A , B >. ) e. ( aleph ` D ) ) with typecode |-
66		alephsdom	Could not format ( ( ( _J0 ` <. A , B >. ) e. On /\ D e. On ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` D ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) ) : No typesetting found for |- ( ( ( _J0 ` <. A , B >. ) e. On /\ D e. On ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` D ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) ) with typecode |-
67	53 31 66	sylancr	Could not format ( A e. ( aleph ` D ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` D ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) ) : No typesetting found for |- ( A e. ( aleph ` D ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` D ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) ) with typecode |-
68	67	adantr	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` D ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) ) -> ( ( _J0 ` <. A , B >. ) e. ( aleph ` D ) <-> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) ) with typecode |-
69	65 68	mpbid	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) with typecode |-
70	69	3adant3	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) with typecode |-
71	70	adantr	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) with typecode |-
72		ensdomtr	Could not format ( ( ( _J ` <. A , B , C >. ) ~~ ( _J0 ` <. A , B >. ) /\ ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) -> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) : No typesetting found for |- ( ( ( _J ` <. A , B , C >. ) ~~ ( _J0 ` <. A , B >. ) /\ ( _J0 ` <. A , B >. ) ~< ( aleph ` D ) ) -> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) with typecode |-
73	64 71 72	syl2anc	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) with typecode |-
74		jf1	Could not format _J : ( ( On X. On ) X. 9o ) -1-1-> On : No typesetting found for |- _J : ( ( On X. On ) X. 9o ) -1-1-> On with typecode |-
75		f1f	Could not format ( _J : ( ( On X. On ) X. 9o ) -1-1-> On -> _J : ( ( On X. On ) X. 9o ) --> On ) : No typesetting found for |- ( _J : ( ( On X. On ) X. 9o ) -1-1-> On -> _J : ( ( On X. On ) X. 9o ) --> On ) with typecode |-
76	74 75	ax-mp	Could not format _J : ( ( On X. On ) X. 9o ) --> On : No typesetting found for |- _J : ( ( On X. On ) X. 9o ) --> On with typecode |-
77	76 52	f0cli	Could not format ( _J ` <. A , B , C >. ) e. On : No typesetting found for |- ( _J ` <. A , B , C >. ) e. On with typecode |-
78		alephsdom	Could not format ( ( ( _J ` <. A , B , C >. ) e. On /\ D e. On ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) ) : No typesetting found for |- ( ( ( _J ` <. A , B , C >. ) e. On /\ D e. On ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) ) with typecode |-
79	77 31 78	sylancr	Could not format ( A e. ( aleph ` D ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) ) : No typesetting found for |- ( A e. ( aleph ` D ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) ) with typecode |-
80	79	3ad2ant1	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) ) with typecode |-
81	80	adantr	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( ( _J ` <. A , B , C >. ) e. ( aleph ` D ) <-> ( _J ` <. A , B , C >. ) ~< ( aleph ` D ) ) ) with typecode |-
82	73 81	mpbird	Could not format ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) ) : No typesetting found for |- ( ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) /\ -. ( _J0 ` <. A , B >. ) e. _om ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) ) with typecode |-
83	46 82	pm2.61dan	Could not format ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) ) : No typesetting found for |- ( ( A e. ( aleph ` D ) /\ B e. ( aleph ` D ) /\ C e. 9o ) -> ( _J ` <. A , B , C >. ) e. ( aleph ` D ) ) with typecode |-