Theorem jf1o

Description: _J is a bijection from ( ( On X. On ) X. 9o ) to On . Proposition 15.3 of TakeutiZaring p. 155. (Contributed by BTernaryTau, 6-Oct-2026)

	Ref	Expression
Assertion	jf1o	Could not format assertion : No typesetting found for |- _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On with typecode |-

Proof

Step	Hyp	Ref	Expression
1		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 |-
2		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 |-
3		frn	Could not format ( _J : ( ( On X. On ) X. 9o ) --> On -> ran _J C_ On ) : No typesetting found for |- ( _J : ( ( On X. On ) X. 9o ) --> On -> ran _J C_ On ) with typecode |-
4	1 2 3	mp2b	Could not format ran _J C_ On : No typesetting found for |- ran _J C_ On with typecode |-
5		ssab	Could not format ( On C_ { w | E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) } <-> A. w ( w e. On -> E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) ) : No typesetting found for |- ( On C_ { w | E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) } <-> A. w ( w e. On -> E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) ) with typecode |-
6		9on	Could not format 9o e. On : No typesetting found for |- 9o e. On with typecode |-
7		df-9o	Could not format 9o = suc 8o : No typesetting found for |- 9o = suc 8o with typecode |-
8		nsuceq0	Could not format suc 8o =/= (/) : No typesetting found for |- suc 8o =/= (/) with typecode |-
9	7 8	eqnetri	Could not format 9o =/= (/) : No typesetting found for |- 9o =/= (/) with typecode |-
10		omeulem1	Could not format ( ( 9o e. On /\ w e. On /\ 9o =/= (/) ) -> E. t e. On E. v e. 9o ( ( 9o .o t ) +o v ) = w ) : No typesetting found for |- ( ( 9o e. On /\ w e. On /\ 9o =/= (/) ) -> E. t e. On E. v e. 9o ( ( 9o .o t ) +o v ) = w ) with typecode |-
11	6 9 10	mp3an13	Could not format ( w e. On -> E. t e. On E. v e. 9o ( ( 9o .o t ) +o v ) = w ) : No typesetting found for |- ( w e. On -> E. t e. On E. v e. 9o ( ( 9o .o t ) +o v ) = w ) with typecode |-
12		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 |-
13		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 |-
14		f1ofo	Could not format ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) -onto-> On ) : No typesetting found for |- ( _J0 : ( On X. On ) -1-1-onto-> On -> _J0 : ( On X. On ) -onto-> On ) with typecode |-
15	12 13 14	mp2b	Could not format _J0 : ( On X. On ) -onto-> On : No typesetting found for |- _J0 : ( On X. On ) -onto-> On with typecode |-
16		foelcdmi	Could not format ( ( _J0 : ( On X. On ) -onto-> On /\ t e. On ) -> E. u e. ( On X. On ) ( _J0 ` u ) = t ) : No typesetting found for |- ( ( _J0 : ( On X. On ) -onto-> On /\ t e. On ) -> E. u e. ( On X. On ) ( _J0 ` u ) = t ) with typecode |-
17	15 16	mpan	Could not format ( t e. On -> E. u e. ( On X. On ) ( _J0 ` u ) = t ) : No typesetting found for |- ( t e. On -> E. u e. ( On X. On ) ( _J0 ` u ) = t ) with typecode |-
18		oveq2	Could not format ( ( _J0 ` u ) = t -> ( 9o .o ( _J0 ` u ) ) = ( 9o .o t ) ) : No typesetting found for |- ( ( _J0 ` u ) = t -> ( 9o .o ( _J0 ` u ) ) = ( 9o .o t ) ) with typecode |-
19	18	oveq1d	Could not format ( ( _J0 ` u ) = t -> ( ( 9o .o ( _J0 ` u ) ) +o v ) = ( ( 9o .o t ) +o v ) ) : No typesetting found for |- ( ( _J0 ` u ) = t -> ( ( 9o .o ( _J0 ` u ) ) +o v ) = ( ( 9o .o t ) +o v ) ) with typecode |-
20	19	eqeq2d	Could not format ( ( _J0 ` u ) = t -> ( w = ( ( 9o .o ( _J0 ` u ) ) +o v ) <-> w = ( ( 9o .o t ) +o v ) ) ) : No typesetting found for |- ( ( _J0 ` u ) = t -> ( w = ( ( 9o .o ( _J0 ` u ) ) +o v ) <-> w = ( ( 9o .o t ) +o v ) ) ) with typecode |-
21		eqcom	Could not format ( w = ( ( 9o .o t ) +o v ) <-> ( ( 9o .o t ) +o v ) = w ) : No typesetting found for |- ( w = ( ( 9o .o t ) +o v ) <-> ( ( 9o .o t ) +o v ) = w ) with typecode |-
22	20 21	bitrdi	Could not format ( ( _J0 ` u ) = t -> ( w = ( ( 9o .o ( _J0 ` u ) ) +o v ) <-> ( ( 9o .o t ) +o v ) = w ) ) : No typesetting found for |- ( ( _J0 ` u ) = t -> ( w = ( ( 9o .o ( _J0 ` u ) ) +o v ) <-> ( ( 9o .o t ) +o v ) = w ) ) with typecode |-
23	22	rexbidv	Could not format ( ( _J0 ` u ) = t -> ( E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) <-> E. v e. 9o ( ( 9o .o t ) +o v ) = w ) ) : No typesetting found for |- ( ( _J0 ` u ) = t -> ( E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) <-> E. v e. 9o ( ( 9o .o t ) +o v ) = w ) ) with typecode |-
24	23	biimprcd	Could not format ( E. v e. 9o ( ( 9o .o t ) +o v ) = w -> ( ( _J0 ` u ) = t -> E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) ) : No typesetting found for |- ( E. v e. 9o ( ( 9o .o t ) +o v ) = w -> ( ( _J0 ` u ) = t -> E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) ) with typecode |-
25	24	reximdv	Could not format ( E. v e. 9o ( ( 9o .o t ) +o v ) = w -> ( E. u e. ( On X. On ) ( _J0 ` u ) = t -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) ) : No typesetting found for |- ( E. v e. 9o ( ( 9o .o t ) +o v ) = w -> ( E. u e. ( On X. On ) ( _J0 ` u ) = t -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) ) with typecode |-
26	17 25	mpan9	Could not format ( ( t e. On /\ E. v e. 9o ( ( 9o .o t ) +o v ) = w ) -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) : No typesetting found for |- ( ( t e. On /\ E. v e. 9o ( ( 9o .o t ) +o v ) = w ) -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) with typecode |-
27	26	rexlimiva	Could not format ( E. t e. On E. v e. 9o ( ( 9o .o t ) +o v ) = w -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) : No typesetting found for |- ( E. t e. On E. v e. 9o ( ( 9o .o t ) +o v ) = w -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) with typecode |-
28	11 27	syl	Could not format ( w e. On -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) : No typesetting found for |- ( w e. On -> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) with typecode |-
29		vex	$$⊢u\in \mathrm{V}$$
30		vex	$$⊢v\in \mathrm{V}$$
31	29 30	op1std	$$⊢z=⟨u,v⟩\to 1^{st}\left(z\right)=u$$
32	31	fveq2d	Could not format ( z = <. u , v >. -> ( _J0 ` ( 1st ` z ) ) = ( _J0 ` u ) ) : No typesetting found for |- ( z = <. u , v >. -> ( _J0 ` ( 1st ` z ) ) = ( _J0 ` u ) ) with typecode |-
33	32	oveq2d	Could not format ( z = <. u , v >. -> ( 9o .o ( _J0 ` ( 1st ` z ) ) ) = ( 9o .o ( _J0 ` u ) ) ) : No typesetting found for |- ( z = <. u , v >. -> ( 9o .o ( _J0 ` ( 1st ` z ) ) ) = ( 9o .o ( _J0 ` u ) ) ) with typecode |-
34	29 30	op2ndd	$$⊢z=⟨u,v⟩\to 2^{nd}\left(z\right)=v$$
35	33 34	oveq12d	Could not format ( z = <. u , v >. -> ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) : No typesetting found for |- ( z = <. u , v >. -> ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) with typecode |-
36	35	eqeq2d	Could not format ( z = <. u , v >. -> ( w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) <-> w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) ) : No typesetting found for |- ( z = <. u , v >. -> ( w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) <-> w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) ) with typecode |-
37	36	rexxp	Could not format ( E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) <-> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) : No typesetting found for |- ( E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) <-> E. u e. ( On X. On ) E. v e. 9o w = ( ( 9o .o ( _J0 ` u ) ) +o v ) ) with typecode |-
38	28 37	sylibr	Could not format ( w e. On -> E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) : No typesetting found for |- ( w e. On -> E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) with typecode |-
39	5 38	mpgbir	Could not format On C_ { w | E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) } : No typesetting found for |- On C_ { w | E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) } with typecode |-
40		dfj2	Could not format _J = ( z e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) : No typesetting found for |- _J = ( z e. ( ( On X. On ) X. 9o ) |-> ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) ) with typecode |-
41	40	rnmpt	Could not format ran _J = { w | E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) } : No typesetting found for |- ran _J = { w | E. z e. ( ( On X. On ) X. 9o ) w = ( ( 9o .o ( _J0 ` ( 1st ` z ) ) ) +o ( 2nd ` z ) ) } with typecode |-
42	39 41	sseqtrri	Could not format On C_ ran _J : No typesetting found for |- On C_ ran _J with typecode |-
43	4 42	eqssi	Could not format ran _J = On : No typesetting found for |- ran _J = On with typecode |-
44		dff1o5	Could not format ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On <-> ( _J : ( ( On X. On ) X. 9o ) -1-1-> On /\ ran _J = On ) ) : No typesetting found for |- ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On <-> ( _J : ( ( On X. On ) X. 9o ) -1-1-> On /\ ran _J = On ) ) with typecode |-
45	1 43 44	mpbir2an	Could not format _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On : No typesetting found for |- _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On with typecode |-