Theorem jf1

Description: _J is a one-to-one function. Part of Proposition 15.3 of TakeutiZaring p. 155. (Contributed by BTernaryTau, 6-Oct-2026)

	Ref	Expression
Assertion	jf1	Could not format assertion : No typesetting found for |- _J : ( ( On X. On ) X. 9o ) -1-1-> On 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	2 3	ax-mp	Could not format _J0 : ( On X. On ) -1-1-onto-> On : No typesetting found for |- _J0 : ( On X. On ) -1-1-onto-> On with typecode |-
5		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 |-
6	4 5	ax-mp	Could not format _J0 : ( On X. On ) --> On : No typesetting found for |- _J0 : ( On X. On ) --> On with typecode |-
7		0elon	$$⊢\varnothing \in \mathrm{On}$$
8	6 7	f0cli	Could not format ( _J0 ` ( 1st ` w ) ) e. On : No typesetting found for |- ( _J0 ` ( 1st ` w ) ) e. On with typecode |-
9		omcl	Could not format ( ( 9o e. On /\ ( _J0 ` ( 1st ` w ) ) e. On ) -> ( 9o .o ( _J0 ` ( 1st ` w ) ) ) e. On ) : No typesetting found for |- ( ( 9o e. On /\ ( _J0 ` ( 1st ` w ) ) e. On ) -> ( 9o .o ( _J0 ` ( 1st ` w ) ) ) e. On ) with typecode |-
10	1 8 9	mp2an	Could not format ( 9o .o ( _J0 ` ( 1st ` w ) ) ) e. On : No typesetting found for |- ( 9o .o ( _J0 ` ( 1st ` w ) ) ) e. On with typecode |-
11		xp2nd	Could not format ( w e. ( ( On X. On ) X. 9o ) -> ( 2nd ` w ) e. 9o ) : No typesetting found for |- ( w e. ( ( On X. On ) X. 9o ) -> ( 2nd ` w ) e. 9o ) with typecode |-
12		onelon	Could not format ( ( 9o e. On /\ ( 2nd ` w ) e. 9o ) -> ( 2nd ` w ) e. On ) : No typesetting found for |- ( ( 9o e. On /\ ( 2nd ` w ) e. 9o ) -> ( 2nd ` w ) e. On ) with typecode |-
13	1 11 12	sylancr	Could not format ( w e. ( ( On X. On ) X. 9o ) -> ( 2nd ` w ) e. On ) : No typesetting found for |- ( w e. ( ( On X. On ) X. 9o ) -> ( 2nd ` w ) e. On ) with typecode |-
14		oacl	Could not format ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) e. On /\ ( 2nd ` w ) e. On ) -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On ) : No typesetting found for |- ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) e. On /\ ( 2nd ` w ) e. On ) -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On ) with typecode |-
15	10 13 14	sylancr	Could not format ( w e. ( ( On X. On ) X. 9o ) -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On ) : No typesetting found for |- ( w e. ( ( On X. On ) X. 9o ) -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On ) with typecode |-
16	15	rgen	Could not format A. w e. ( ( On X. On ) X. 9o ) ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On : No typesetting found for |- A. w e. ( ( On X. On ) X. 9o ) ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On with typecode |-
17	1	a1i	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> 9o e. On ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> 9o e. On ) with typecode |-
18		df-9o	Could not format 9o = suc 8o : No typesetting found for |- 9o = suc 8o with typecode |-
19		nsuceq0	Could not format suc 8o =/= (/) : No typesetting found for |- suc 8o =/= (/) with typecode |-
20	18 19	eqnetri	Could not format 9o =/= (/) : No typesetting found for |- 9o =/= (/) with typecode |-
21	20	a1i	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> 9o =/= (/) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> 9o =/= (/) ) with typecode |-
22	8	a1i	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( _J0 ` ( 1st ` w ) ) e. On ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( _J0 ` ( 1st ` w ) ) e. On ) with typecode |-
23	11	3ad2ant1	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( 2nd ` w ) e. 9o ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( 2nd ` w ) e. 9o ) with typecode |-
24	6 7	f0cli	Could not format ( _J0 ` ( 1st ` z ) ) e. On : No typesetting found for |- ( _J0 ` ( 1st ` z ) ) e. On with typecode |-
25	24	a1i	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( _J0 ` ( 1st ` z ) ) e. On ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( _J0 ` ( 1st ` z ) ) e. On ) with typecode |-
26		xp2nd	Could not format ( z e. ( ( On X. On ) X. 9o ) -> ( 2nd ` z ) e. 9o ) : No typesetting found for |- ( z e. ( ( On X. On ) X. 9o ) -> ( 2nd ` z ) e. 9o ) with typecode |-
27	26	3ad2ant2	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( 2nd ` z ) e. 9o ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( 2nd ` z ) e. 9o ) with typecode |-
28		simp3	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) with typecode |-
29	17 21 22 23 25 27 28	omeueq	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) with typecode |-
30		xp1st	Could not format ( w e. ( ( On X. On ) X. 9o ) -> ( 1st ` w ) e. ( On X. On ) ) : No typesetting found for |- ( w e. ( ( On X. On ) X. 9o ) -> ( 1st ` w ) e. ( On X. On ) ) with typecode |-
31		xp1st	Could not format ( z e. ( ( On X. On ) X. 9o ) -> ( 1st ` z ) e. ( On X. On ) ) : No typesetting found for |- ( z e. ( ( On X. On ) X. 9o ) -> ( 1st ` z ) e. ( On X. On ) ) with typecode |-
32		f1of1	Could not format ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) -1-1-> On ) : No typesetting found for |- ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) -1-1-> On ) with typecode |-
33	4 32	ax-mp	Could not format _J0 : ( On X. On ) -1-1-> On : No typesetting found for |- _J0 : ( On X. On ) -1-1-> On with typecode |-
34		f1veqaeq	Could not format ( ( _J0 : ( On X. On ) -1-1-> On /\ ( ( 1st ` w ) e. ( On X. On ) /\ ( 1st ` z ) e. ( On X. On ) ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) -> ( 1st ` w ) = ( 1st ` z ) ) ) : No typesetting found for |- ( ( _J0 : ( On X. On ) -1-1-> On /\ ( ( 1st ` w ) e. ( On X. On ) /\ ( 1st ` z ) e. ( On X. On ) ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) -> ( 1st ` w ) = ( 1st ` z ) ) ) with typecode |-
35	33 34	mpan	Could not format ( ( ( 1st ` w ) e. ( On X. On ) /\ ( 1st ` z ) e. ( On X. On ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) -> ( 1st ` w ) = ( 1st ` z ) ) ) : No typesetting found for |- ( ( ( 1st ` w ) e. ( On X. On ) /\ ( 1st ` z ) e. ( On X. On ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) -> ( 1st ` w ) = ( 1st ` z ) ) ) with typecode |-
36	30 31 35	syl2an	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) -> ( 1st ` w ) = ( 1st ` z ) ) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) -> ( 1st ` w ) = ( 1st ` z ) ) ) with typecode |-
37	36	anim1d	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) -> ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) -> ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) ) with typecode |-
38	37	3adant3	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) -> ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) -> ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) ) with typecode |-
39	29 38	mpd	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) ) with typecode |-
40		xpopth	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) <-> w = z ) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) <-> w = z ) ) with typecode |-
41	40	3adant3	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) <-> w = z ) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> ( ( ( 1st ` w ) = ( 1st ` z ) /\ ( 2nd ` w ) = ( 2nd ` z ) ) <-> w = z ) ) with typecode |-
42	39 41	mpbid	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> w = z ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) /\ ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) -> w = z ) with typecode |-
43	42	3expia	Could not format ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) -> w = z ) ) : No typesetting found for |- ( ( w e. ( ( On X. On ) X. 9o ) /\ z e. ( ( On X. On ) X. 9o ) ) -> ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) -> w = z ) ) with typecode |-
44	43	rgen2	Could not format A. w e. ( ( On X. On ) X. 9o ) A. z e. ( ( On X. On ) X. 9o ) ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) -> w = z ) : No typesetting found for |- A. w e. ( ( On X. On ) X. 9o ) A. z e. ( ( On X. On ) X. 9o ) ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) -> w = z ) with typecode |-
45		dfj2	Could not format _J = ( w e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) ) : No typesetting found for |- _J = ( w e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) ) with typecode |-
46		2fveq3	Could not format ( w = z -> ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) ) : No typesetting found for |- ( w = z -> ( _J0 ` ( 1st ` w ) ) = ( _J0 ` ( 1st ` z ) ) ) with typecode |-
47	46	oveq2d	Could not format ( w = z -> ( 9o .o ( _J0 ` ( 1st ` w ) ) ) = ( 9o .o ( _J0 ` ( 1st ` z ) ) ) ) : No typesetting found for |- ( w = z -> ( 9o .o ( _J0 ` ( 1st ` w ) ) ) = ( 9o .o ( _J0 ` ( 1st ` z ) ) ) ) with typecode |-
48		fveq2	$$⊢w=z\to 2^{nd}\left(w\right)=2^{nd}\left(z\right)$$
49	47 48	oveq12d	Could not format ( w = z -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) : No typesetting found for |- ( w = z -> ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) with typecode |-
50	45 49	f1mpt	Could not format ( _J : ( ( On X. On ) X. 9o ) -1-1-> On <-> ( A. w e. ( ( On X. On ) X. 9o ) ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On /\ A. w e. ( ( On X. On ) X. 9o ) A. z e. ( ( On X. On ) X. 9o ) ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) -> w = z ) ) ) : No typesetting found for |- ( _J : ( ( On X. On ) X. 9o ) -1-1-> On <-> ( A. w e. ( ( On X. On ) X. 9o ) ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) e. On /\ A. w e. ( ( On X. On ) X. 9o ) A. z e. ( ( On X. On ) X. 9o ) ( ( ( 9o .o ( _J0 ` ( 1st ` w ) ) ) +o ( 2nd ` w ) ) = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) -> w = z ) ) ) with typecode |-
51	16 44 50	mpbir2an	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 |-