Theorem j0ltalephlem

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

	Ref	Expression
Assertion	j0ltalephlem	Could not format assertion : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		fvex	Could not format ( _J0 ` <. A , B >. ) e. _V : No typesetting found for |- ( _J0 ` <. A , B >. ) e. _V 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		opelxpi	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to ⟨A,B⟩\in \left(\mathrm{On}\times \mathrm{On}\right)$$
4		imassrn	Could not format ( `' _R0 " { <. A , B >. } ) C_ ran `' _R0 : No typesetting found for |- ( `' _R0 " { <. A , B >. } ) C_ ran `' _R0 with typecode |-
5		dfdm4	Could not format dom _R0 = ran `' _R0 : No typesetting found for |- dom _R0 = ran `' _R0 with typecode |-
6		dmr0ss	Could not format dom _R0 C_ ( On X. On ) : No typesetting found for |- dom _R0 C_ ( On X. On ) with typecode |-
7	5 6	eqsstrri	Could not format ran `' _R0 C_ ( On X. On ) : No typesetting found for |- ran `' _R0 C_ ( On X. On ) with typecode |-
8	4 7	sstri	Could not format ( `' _R0 " { <. A , B >. } ) C_ ( On X. On ) : No typesetting found for |- ( `' _R0 " { <. A , B >. } ) C_ ( On X. On ) with typecode |-
9		sseqin2	Could not format ( ( `' _R0 " { <. A , B >. } ) C_ ( On X. On ) <-> ( ( On X. On ) i^i ( `' _R0 " { <. A , B >. } ) ) = ( `' _R0 " { <. A , B >. } ) ) : No typesetting found for |- ( ( `' _R0 " { <. A , B >. } ) C_ ( On X. On ) <-> ( ( On X. On ) i^i ( `' _R0 " { <. A , B >. } ) ) = ( `' _R0 " { <. A , B >. } ) ) with typecode |-
10	8 9	mpbi	Could not format ( ( On X. On ) i^i ( `' _R0 " { <. A , B >. } ) ) = ( `' _R0 " { <. A , B >. } ) : No typesetting found for |- ( ( On X. On ) i^i ( `' _R0 " { <. A , B >. } ) ) = ( `' _R0 " { <. A , B >. } ) with typecode |-
11	10	eqcomi	Could not format ( `' _R0 " { <. A , B >. } ) = ( ( On X. On ) i^i ( `' _R0 " { <. A , B >. } ) ) : No typesetting found for |- ( `' _R0 " { <. A , B >. } ) = ( ( On X. On ) i^i ( `' _R0 " { <. A , B >. } ) ) with typecode |-
12	1	epini	Could not format ( `' _E " { ( _J0 ` <. A , B >. ) } ) = ( _J0 ` <. A , B >. ) : No typesetting found for |- ( `' _E " { ( _J0 ` <. A , B >. ) } ) = ( _J0 ` <. A , B >. ) with typecode |-
13	12	ineq2i	Could not format ( On i^i ( `' _E " { ( _J0 ` <. A , B >. ) } ) ) = ( On i^i ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( On i^i ( `' _E " { ( _J0 ` <. A , B >. ) } ) ) = ( On i^i ( _J0 ` <. A , B >. ) ) with typecode |-
14		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 |-
15		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 |-
16	2 14 15	mp2b	Could not format _J0 : ( On X. On ) --> On : No typesetting found for |- _J0 : ( On X. On ) --> On with typecode |-
17		0elon	$$⊢\varnothing \in \mathrm{On}$$
18	16 17	f0cli	Could not format ( _J0 ` <. A , B >. ) e. On : No typesetting found for |- ( _J0 ` <. A , B >. ) e. On with typecode |-
19	18	onssi	Could not format ( _J0 ` <. A , B >. ) C_ On : No typesetting found for |- ( _J0 ` <. A , B >. ) C_ On with typecode |-
20		sseqin2	Could not format ( ( _J0 ` <. A , B >. ) C_ On <-> ( On i^i ( _J0 ` <. A , B >. ) ) = ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( _J0 ` <. A , B >. ) C_ On <-> ( On i^i ( _J0 ` <. A , B >. ) ) = ( _J0 ` <. A , B >. ) ) with typecode |-
21	19 20	mpbi	Could not format ( On i^i ( _J0 ` <. A , B >. ) ) = ( _J0 ` <. A , B >. ) : No typesetting found for |- ( On i^i ( _J0 ` <. A , B >. ) ) = ( _J0 ` <. A , B >. ) with typecode |-
22	13 21	eqtr2i	Could not format ( _J0 ` <. A , B >. ) = ( On i^i ( `' _E " { ( _J0 ` <. A , B >. ) } ) ) : No typesetting found for |- ( _J0 ` <. A , B >. ) = ( On i^i ( `' _E " { ( _J0 ` <. A , B >. ) } ) ) with typecode |-
23	11 22	isoini2	Could not format ( ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) /\ <. A , B >. e. ( On X. On ) ) -> ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) Isom _R0 , _E ( ( `' _R0 " { <. A , B >. } ) , ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( _J0 Isom _R0 , _E ( ( On X. On ) , On ) /\ <. A , B >. e. ( On X. On ) ) -> ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) Isom _R0 , _E ( ( `' _R0 " { <. A , B >. } ) , ( _J0 ` <. A , B >. ) ) ) with typecode |-
24	2 3 23	sylancr	Could not format ( ( A e. On /\ B e. On ) -> ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) Isom _R0 , _E ( ( `' _R0 " { <. A , B >. } ) , ( _J0 ` <. A , B >. ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) Isom _R0 , _E ( ( `' _R0 " { <. A , B >. } ) , ( _J0 ` <. A , B >. ) ) ) with typecode |-
25		isof1o	Could not format ( ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) Isom _R0 , _E ( ( `' _R0 " { <. A , B >. } ) , ( _J0 ` <. A , B >. ) ) -> ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( `' _R0 " { <. A , B >. } ) -1-1-onto-> ( _J0 ` <. A , B >. ) ) : No typesetting found for |- ( ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) Isom _R0 , _E ( ( `' _R0 " { <. A , B >. } ) , ( _J0 ` <. A , B >. ) ) -> ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( `' _R0 " { <. A , B >. } ) -1-1-onto-> ( _J0 ` <. A , B >. ) ) with typecode |-
26		f1ocnv	Could not format ( ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( `' _R0 " { <. A , B >. } ) -1-1-onto-> ( _J0 ` <. A , B >. ) -> `' ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( _J0 ` <. A , B >. ) -1-1-onto-> ( `' _R0 " { <. A , B >. } ) ) : No typesetting found for |- ( ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( `' _R0 " { <. A , B >. } ) -1-1-onto-> ( _J0 ` <. A , B >. ) -> `' ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( _J0 ` <. A , B >. ) -1-1-onto-> ( `' _R0 " { <. A , B >. } ) ) with typecode |-
27	24 25 26	3syl	Could not format ( ( A e. On /\ B e. On ) -> `' ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( _J0 ` <. A , B >. ) -1-1-onto-> ( `' _R0 " { <. A , B >. } ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> `' ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( _J0 ` <. A , B >. ) -1-1-onto-> ( `' _R0 " { <. A , B >. } ) ) with typecode |-
28		f1oeng	Could not format ( ( ( _J0 ` <. A , B >. ) e. _V /\ `' ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( _J0 ` <. A , B >. ) -1-1-onto-> ( `' _R0 " { <. A , B >. } ) ) -> ( _J0 ` <. A , B >. ) ~~ ( `' _R0 " { <. A , B >. } ) ) : No typesetting found for |- ( ( ( _J0 ` <. A , B >. ) e. _V /\ `' ( _J0 |` ( `' _R0 " { <. A , B >. } ) ) : ( _J0 ` <. A , B >. ) -1-1-onto-> ( `' _R0 " { <. A , B >. } ) ) -> ( _J0 ` <. A , B >. ) ~~ ( `' _R0 " { <. A , B >. } ) ) with typecode |-
29	1 27 28	sylancr	Could not format ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~~ ( `' _R0 " { <. A , B >. } ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~~ ( `' _R0 " { <. A , B >. } ) ) with typecode |-
30		onun2	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A\cup B\in \mathrm{On}$$
31		onsuc	$$⊢A\cup B\in \mathrm{On}\to \mathrm{suc}\left(A\cup B\right)\in \mathrm{On}$$
32	30 31	syl	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \mathrm{suc}\left(A\cup B\right)\in \mathrm{On}$$
33	32 32	xpexd	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to \mathrm{suc}\left(A\cup B\right)\times \mathrm{suc}\left(A\cup B\right)\in \mathrm{V}$$
34		simplrl	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> x e. On ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> x e. On ) with typecode |-
35		simplrr	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> y e. On ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> y e. On ) with typecode |-
36		simplll	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> A e. On ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> A e. On ) with typecode |-
37		simpllr	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> B e. On ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> B e. On ) with typecode |-
38		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
39		opex	$$⊢⟨x,y⟩\in \mathrm{V}$$
40	39	eliniseg	Could not format ( <. A , B >. e. _V -> ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) <-> <. x , y >. _R0 <. A , B >. ) ) : No typesetting found for |- ( <. A , B >. e. _V -> ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) <-> <. x , y >. _R0 <. A , B >. ) ) with typecode |-
41	38 40	ax-mp	Could not format ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) <-> <. x , y >. _R0 <. A , B >. ) : No typesetting found for |- ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) <-> <. x , y >. _R0 <. A , B >. ) with typecode |-
42	41	bilani	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> <. x , y >. _R0 <. A , B >. ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> <. x , y >. _R0 <. A , B >. ) with typecode |-
43	34 35 36 37 42	r0maxss	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( x u. y ) C_ ( A u. B ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( x u. y ) C_ ( A u. B ) ) with typecode |-
44	43	unssad	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> x C_ ( A u. B ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> x C_ ( A u. B ) ) with typecode |-
45	36 37 30	syl2anc	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( A u. B ) e. On ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( A u. B ) e. On ) with typecode |-
46		onsssuc	$$⊢\left(x\in \mathrm{On}\wedge A\cup B\in \mathrm{On}\right)\to \left(x\subseteq A\cup B\leftrightarrow x\in \mathrm{suc}\left(A\cup B\right)\right)$$
47	34 45 46	syl2anc	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( x C_ ( A u. B ) <-> x e. suc ( A u. B ) ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( x C_ ( A u. B ) <-> x e. suc ( A u. B ) ) ) with typecode |-
48	44 47	mpbid	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> x e. suc ( A u. B ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> x e. suc ( A u. B ) ) with typecode |-
49	43	unssbd	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> y C_ ( A u. B ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> y C_ ( A u. B ) ) with typecode |-
50		onsssuc	$$⊢\left(y\in \mathrm{On}\wedge A\cup B\in \mathrm{On}\right)\to \left(y\subseteq A\cup B\leftrightarrow y\in \mathrm{suc}\left(A\cup B\right)\right)$$
51	35 45 50	syl2anc	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( y C_ ( A u. B ) <-> y e. suc ( A u. B ) ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> ( y C_ ( A u. B ) <-> y e. suc ( A u. B ) ) ) with typecode |-
52	49 51	mpbid	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> y e. suc ( A u. B ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> y e. suc ( A u. B ) ) with typecode |-
53	48 52	opelxpd	Could not format ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) : No typesetting found for |- ( ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) /\ <. x , y >. e. ( `' _R0 " { <. A , B >. } ) ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) with typecode |-
54	53	ex	Could not format ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) -> ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) : No typesetting found for |- ( ( ( A e. On /\ B e. On ) /\ ( x e. On /\ y e. On ) ) -> ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) with typecode |-
55	54	ralrimivva	Could not format ( ( A e. On /\ B e. On ) -> A. x e. On A. y e. On ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> A. x e. On A. y e. On ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) with typecode |-
56		ssrel2	Could not format ( ( `' _R0 " { <. A , B >. } ) C_ ( On X. On ) -> ( ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) <-> A. x e. On A. y e. On ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) ) : No typesetting found for |- ( ( `' _R0 " { <. A , B >. } ) C_ ( On X. On ) -> ( ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) <-> A. x e. On A. y e. On ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) ) with typecode |-
57	8 56	ax-mp	Could not format ( ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) <-> A. x e. On A. y e. On ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) : No typesetting found for |- ( ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) <-> A. x e. On A. y e. On ( <. x , y >. e. ( `' _R0 " { <. A , B >. } ) -> <. x , y >. e. ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) with typecode |-
58	55 57	sylibr	Could not format ( ( A e. On /\ B e. On ) -> ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) with typecode |-
59		ssdomg	Could not format ( ( suc ( A u. B ) X. suc ( A u. B ) ) e. _V -> ( ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) -> ( `' _R0 " { <. A , B >. } ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) : No typesetting found for |- ( ( suc ( A u. B ) X. suc ( A u. B ) ) e. _V -> ( ( `' _R0 " { <. A , B >. } ) C_ ( suc ( A u. B ) X. suc ( A u. B ) ) -> ( `' _R0 " { <. A , B >. } ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) ) with typecode |-
60	33 58 59	sylc	Could not format ( ( A e. On /\ B e. On ) -> ( `' _R0 " { <. A , B >. } ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( `' _R0 " { <. A , B >. } ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) with typecode |-
61		endomtr	Could not format ( ( ( _J0 ` <. A , B >. ) ~~ ( `' _R0 " { <. A , B >. } ) /\ ( `' _R0 " { <. A , B >. } ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) : No typesetting found for |- ( ( ( _J0 ` <. A , B >. ) ~~ ( `' _R0 " { <. A , B >. } ) /\ ( `' _R0 " { <. A , B >. } ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) with typecode |-
62	29 60 61	syl2anc	Could not format ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) : No typesetting found for |- ( ( A e. On /\ B e. On ) -> ( _J0 ` <. A , B >. ) ~<_ ( suc ( A u. B ) X. suc ( A u. B ) ) ) with typecode |-