Theorem dfk22

Description: Alternate definition of _K2 using maps-to notation. (Contributed by BTernaryTau, 10-Oct-2026)

	Ref	Expression
Assertion	dfk22	Could not format assertion : No typesetting found for |- _K2 = ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		simpl	Could not format ( ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) -> x e. On ) : No typesetting found for |- ( ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) -> x e. On ) with typecode |-
2		simpr	Could not format ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> z e. On ) : No typesetting found for |- ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> z e. On ) with typecode |-
3		simpllr	Could not format ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> y e. On ) : No typesetting found for |- ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> y e. On ) with typecode |-
4		simplr	Could not format ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> n e. 9o ) : No typesetting found for |- ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> n e. 9o ) with typecode |-
5		simplll	Could not format ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> x e. On ) : No typesetting found for |- ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> x e. On ) with typecode |-
6		eqcom	Could not format ( x = ( _J ` <. z , y , n >. ) <-> ( _J ` <. z , y , n >. ) = x ) : No typesetting found for |- ( x = ( _J ` <. z , y , n >. ) <-> ( _J ` <. z , y , n >. ) = x ) with typecode |-
7		otelxp	Could not format ( <. z , y , n >. e. ( ( On X. On ) X. 9o ) <-> ( z e. On /\ y e. On /\ n e. 9o ) ) : No typesetting found for |- ( <. z , y , n >. e. ( ( On X. On ) X. 9o ) <-> ( z e. On /\ y e. On /\ n e. 9o ) ) with typecode |-
8		jf1o	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 |-
9		f1ocnvfvb	Could not format ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ <. z , y , n >. e. ( ( On X. On ) X. 9o ) /\ x e. On ) -> ( ( _J ` <. z , y , n >. ) = x <-> ( `' _J ` x ) = <. z , y , n >. ) ) : No typesetting found for |- ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ <. z , y , n >. e. ( ( On X. On ) X. 9o ) /\ x e. On ) -> ( ( _J ` <. z , y , n >. ) = x <-> ( `' _J ` x ) = <. z , y , n >. ) ) with typecode |-
10	8 9	mp3an1	Could not format ( ( <. z , y , n >. e. ( ( On X. On ) X. 9o ) /\ x e. On ) -> ( ( _J ` <. z , y , n >. ) = x <-> ( `' _J ` x ) = <. z , y , n >. ) ) : No typesetting found for |- ( ( <. z , y , n >. e. ( ( On X. On ) X. 9o ) /\ x e. On ) -> ( ( _J ` <. z , y , n >. ) = x <-> ( `' _J ` x ) = <. z , y , n >. ) ) with typecode |-
11	7 10	sylanbr	Could not format ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( ( _J ` <. z , y , n >. ) = x <-> ( `' _J ` x ) = <. z , y , n >. ) ) : No typesetting found for |- ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( ( _J ` <. z , y , n >. ) = x <-> ( `' _J ` x ) = <. z , y , n >. ) ) with typecode |-
12		vex	$$⊢z\in \mathrm{V}$$
13		vex	$$⊢y\in \mathrm{V}$$
14		vex	$$⊢n\in \mathrm{V}$$
15	12 13 14	3pm3.2i	$$⊢\left(z\in \mathrm{V}\wedge y\in \mathrm{V}\wedge n\in \mathrm{V}\right)$$
16		oteqimp	Could not format ( ( `' _J ` x ) = <. z , y , n >. -> ( ( z e. _V /\ y e. _V /\ n e. _V ) -> ( ( 1st ` ( 1st ` ( `' _J ` x ) ) ) = z /\ ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = y /\ ( 2nd ` ( `' _J ` x ) ) = n ) ) ) : No typesetting found for |- ( ( `' _J ` x ) = <. z , y , n >. -> ( ( z e. _V /\ y e. _V /\ n e. _V ) -> ( ( 1st ` ( 1st ` ( `' _J ` x ) ) ) = z /\ ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = y /\ ( 2nd ` ( `' _J ` x ) ) = n ) ) ) with typecode |-
17	15 16	mpi	Could not format ( ( `' _J ` x ) = <. z , y , n >. -> ( ( 1st ` ( 1st ` ( `' _J ` x ) ) ) = z /\ ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = y /\ ( 2nd ` ( `' _J ` x ) ) = n ) ) : No typesetting found for |- ( ( `' _J ` x ) = <. z , y , n >. -> ( ( 1st ` ( 1st ` ( `' _J ` x ) ) ) = z /\ ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = y /\ ( 2nd ` ( `' _J ` x ) ) = n ) ) with typecode |-
18	17	simp2d	Could not format ( ( `' _J ` x ) = <. z , y , n >. -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = y ) : No typesetting found for |- ( ( `' _J ` x ) = <. z , y , n >. -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) = y ) with typecode |-
19	18	eqcomd	Could not format ( ( `' _J ` x ) = <. z , y , n >. -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) : No typesetting found for |- ( ( `' _J ` x ) = <. z , y , n >. -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) with typecode |-
20	11 19	biimtrdi	Could not format ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( ( _J ` <. z , y , n >. ) = x -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) : No typesetting found for |- ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( ( _J ` <. z , y , n >. ) = x -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) with typecode |-
21	6 20	biimtrid	Could not format ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( x = ( _J ` <. z , y , n >. ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) : No typesetting found for |- ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( x = ( _J ` <. z , y , n >. ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) with typecode |-
22	2 3 4 5 21	syl31anc	Could not format ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> ( x = ( _J ` <. z , y , n >. ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> ( x = ( _J ` <. z , y , n >. ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) with typecode |-
23	22	rexlimdva	Could not format ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) -> ( E. z e. On x = ( _J ` <. z , y , n >. ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) : No typesetting found for |- ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) -> ( E. z e. On x = ( _J ` <. z , y , n >. ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) with typecode |-
24	23	rexlimdva	Could not format ( ( x e. On /\ y e. On ) -> ( E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) : No typesetting found for |- ( ( x e. On /\ y e. On ) -> ( E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) with typecode |-
25	24	impr	Could not format ( ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) : No typesetting found for |- ( ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) -> y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) with typecode |-
26	1 25	jca	Could not format ( ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) -> ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) : No typesetting found for |- ( ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) -> ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) with typecode |-
27		f1ocnvdm	Could not format ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ x e. On ) -> ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) ) : No typesetting found for |- ( ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On /\ x e. On ) -> ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) ) with typecode |-
28	8 27	mpan	Could not format ( x e. On -> ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) ) : No typesetting found for |- ( x e. On -> ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) ) with typecode |-
29		xp1st	Could not format ( ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) -> ( 1st ` ( `' _J ` x ) ) e. ( On X. On ) ) : No typesetting found for |- ( ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) -> ( 1st ` ( `' _J ` x ) ) e. ( On X. On ) ) with typecode |-
30		xp2nd	Could not format ( ( 1st ` ( `' _J ` x ) ) e. ( On X. On ) -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) : No typesetting found for |- ( ( 1st ` ( `' _J ` x ) ) e. ( On X. On ) -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) with typecode |-
31	28 29 30	3syl	Could not format ( x e. On -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) : No typesetting found for |- ( x e. On -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) with typecode |-
32	31	adantr	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) with typecode |-
33		eleq1	Could not format ( y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) -> ( y e. On <-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) ) : No typesetting found for |- ( y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) -> ( y e. On <-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) ) with typecode |-
34	33	adantl	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( y e. On <-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( y e. On <-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) ) with typecode |-
35	32 34	mpbird	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> y e. On ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> y e. On ) with typecode |-
36		oteq3	Could not format ( n = ( 2nd ` ( `' _J ` x ) ) -> <. z , y , n >. = <. z , y , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( n = ( 2nd ` ( `' _J ` x ) ) -> <. z , y , n >. = <. z , y , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
37	36	eqeq2d	Could not format ( n = ( 2nd ` ( `' _J ` x ) ) -> ( ( `' _J ` x ) = <. z , y , n >. <-> ( `' _J ` x ) = <. z , y , ( 2nd ` ( `' _J ` x ) ) >. ) ) : No typesetting found for |- ( n = ( 2nd ` ( `' _J ` x ) ) -> ( ( `' _J ` x ) = <. z , y , n >. <-> ( `' _J ` x ) = <. z , y , ( 2nd ` ( `' _J ` x ) ) >. ) ) with typecode |-
38		oteq1	Could not format ( z = ( 1st ` ( 1st ` ( `' _J ` x ) ) ) -> <. z , y , ( 2nd ` ( `' _J ` x ) ) >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( z = ( 1st ` ( 1st ` ( `' _J ` x ) ) ) -> <. z , y , ( 2nd ` ( `' _J ` x ) ) >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
39	38	eqeq2d	Could not format ( z = ( 1st ` ( 1st ` ( `' _J ` x ) ) ) -> ( ( `' _J ` x ) = <. z , y , ( 2nd ` ( `' _J ` x ) ) >. <-> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. ) ) : No typesetting found for |- ( z = ( 1st ` ( 1st ` ( `' _J ` x ) ) ) -> ( ( `' _J ` x ) = <. z , y , ( 2nd ` ( `' _J ` x ) ) >. <-> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. ) ) with typecode |-
40		xp2nd	Could not format ( ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) -> ( 2nd ` ( `' _J ` x ) ) e. 9o ) : No typesetting found for |- ( ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) -> ( 2nd ` ( `' _J ` x ) ) e. 9o ) with typecode |-
41	28 40	syl	Could not format ( x e. On -> ( 2nd ` ( `' _J ` x ) ) e. 9o ) : No typesetting found for |- ( x e. On -> ( 2nd ` ( `' _J ` x ) ) e. 9o ) with typecode |-
42	41	adantr	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( 2nd ` ( `' _J ` x ) ) e. 9o ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( 2nd ` ( `' _J ` x ) ) e. 9o ) with typecode |-
43		xp1st	Could not format ( ( 1st ` ( `' _J ` x ) ) e. ( On X. On ) -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) e. On ) : No typesetting found for |- ( ( 1st ` ( `' _J ` x ) ) e. ( On X. On ) -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) e. On ) with typecode |-
44	28 29 43	3syl	Could not format ( x e. On -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) e. On ) : No typesetting found for |- ( x e. On -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) e. On ) with typecode |-
45	44	adantr	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) e. On ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) e. On ) with typecode |-
46		ot1st2nd	Could not format ( ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( ( `' _J ` x ) e. ( ( On X. On ) X. 9o ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
47	28 46	syl	Could not format ( x e. On -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( x e. On -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
48	47	adantr	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
49		oteq2	Could not format ( y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
50	49	adantl	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
51	48 50	eqtr4d	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
52	37 39 42 45 51	2rspcedvdw	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> E. n e. 9o E. z e. On ( `' _J ` x ) = <. z , y , n >. ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> E. n e. 9o E. z e. On ( `' _J ` x ) = <. z , y , n >. ) with typecode |-
53	11	biimprd	Could not format ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( ( `' _J ` x ) = <. z , y , n >. -> ( _J ` <. z , y , n >. ) = x ) ) : No typesetting found for |- ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( ( `' _J ` x ) = <. z , y , n >. -> ( _J ` <. z , y , n >. ) = x ) ) with typecode |-
54	53 6	imbitrrdi	Could not format ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( ( `' _J ` x ) = <. z , y , n >. -> x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( ( `' _J ` x ) = <. z , y , n >. -> x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
55	2 3 4 5 54	syl31anc	Could not format ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> ( ( `' _J ` x ) = <. z , y , n >. -> x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) /\ z e. On ) -> ( ( `' _J ` x ) = <. z , y , n >. -> x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
56	55	reximdva	Could not format ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) -> ( E. z e. On ( `' _J ` x ) = <. z , y , n >. -> E. z e. On x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( ( x e. On /\ y e. On ) /\ n e. 9o ) -> ( E. z e. On ( `' _J ` x ) = <. z , y , n >. -> E. z e. On x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
57	56	reximdva	Could not format ( ( x e. On /\ y e. On ) -> ( E. n e. 9o E. z e. On ( `' _J ` x ) = <. z , y , n >. -> E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( x e. On /\ y e. On ) -> ( E. n e. 9o E. z e. On ( `' _J ` x ) = <. z , y , n >. -> E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
58	35 57	syldan	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( E. n e. 9o E. z e. On ( `' _J ` x ) = <. z , y , n >. -> E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( E. n e. 9o E. z e. On ( `' _J ` x ) = <. z , y , n >. -> E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
59	52 58	mpd	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) with typecode |-
60	35 59	jca	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
61		f1of	Could not format ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On -> _J : ( ( On X. On ) X. 9o ) --> On ) : No typesetting found for |- ( _J : ( ( On X. On ) X. 9o ) -1-1-onto-> On -> _J : ( ( On X. On ) X. 9o ) --> On ) with typecode |-
62	8 61	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 |-
63		0elon	$$⊢\varnothing \in \mathrm{On}$$
64	62 63	f0cli	Could not format ( _J ` <. z , y , n >. ) e. On : No typesetting found for |- ( _J ` <. z , y , n >. ) e. On with typecode |-
65		eleq1	Could not format ( x = ( _J ` <. z , y , n >. ) -> ( x e. On <-> ( _J ` <. z , y , n >. ) e. On ) ) : No typesetting found for |- ( x = ( _J ` <. z , y , n >. ) -> ( x e. On <-> ( _J ` <. z , y , n >. ) e. On ) ) with typecode |-
66	64 65	mpbiri	Could not format ( x = ( _J ` <. z , y , n >. ) -> x e. On ) : No typesetting found for |- ( x = ( _J ` <. z , y , n >. ) -> x e. On ) with typecode |-
67	66	rexlimivw	Could not format ( E. z e. On x = ( _J ` <. z , y , n >. ) -> x e. On ) : No typesetting found for |- ( E. z e. On x = ( _J ` <. z , y , n >. ) -> x e. On ) with typecode |-
68	67	rexlimivw	Could not format ( E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) -> x e. On ) : No typesetting found for |- ( E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) -> x e. On ) with typecode |-
69	68	adantl	Could not format ( ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) -> x e. On ) : No typesetting found for |- ( ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) -> x e. On ) with typecode |-
70	60 69	jccil	Could not format ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) ) : No typesetting found for |- ( ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) -> ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) ) with typecode |-
71	26 70	impbii	Could not format ( ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) <-> ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) : No typesetting found for |- ( ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) <-> ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) ) with typecode |-
72	71	opabbii	Could not format { <. x , y >. | ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) } = { <. x , y >. | ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) } : No typesetting found for |- { <. x , y >. | ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) } = { <. x , y >. | ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) } with typecode |-
73		df-k2	Could not format _K2 = { <. x , y >. | ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) } : No typesetting found for |- _K2 = { <. x , y >. | ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) } with typecode |-
74	69	pm4.71ri	Could not format ( ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) <-> ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) ) : No typesetting found for |- ( ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) <-> ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) ) with typecode |-
75	74	opabbii	Could not format { <. x , y >. | ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) } = { <. x , y >. | ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) } : No typesetting found for |- { <. x , y >. | ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) } = { <. x , y >. | ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) } with typecode |-
76	73 75	eqtri	Could not format _K2 = { <. x , y >. | ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) } : No typesetting found for |- _K2 = { <. x , y >. | ( x e. On /\ ( y e. On /\ E. n e. 9o E. z e. On x = ( _J ` <. z , y , n >. ) ) ) } with typecode |-
77		df-mpt	Could not format ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) = { <. x , y >. | ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) } : No typesetting found for |- ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) = { <. x , y >. | ( x e. On /\ y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) } with typecode |-
78	72 76 77	3eqtr4i	Could not format _K2 = ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) : No typesetting found for |- _K2 = ( x e. On |-> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) ) with typecode |-