Metamath Proof Explorer

Theorem dfk32

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

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

Proof

Step Hyp Ref Expression
1 simpl Could not format ( ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) -> x e. On ) : No typesetting found for |- ( ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) -> x e. On ) with typecode |-
2 simplr Could not format ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> z e. On ) : No typesetting found for |- ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> z e. On ) with typecode |-
3 simpr Could not format ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> y e. On ) : No typesetting found for |- ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> y e. On ) with typecode |-
4 simpllr Could not format ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> n e. 9o ) : No typesetting found for |- ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> n e. 9o ) with typecode |-
5 simplll Could not format ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> x e. On ) : No typesetting found for |- ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y 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 ∈ V
13 vex ⊢ y ∈ V
14 vex ⊢ n ∈ V
15 12 13 14 3pm3.2i ⊢ z ∈ V ∧ y ∈ V ∧ n ∈ V
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 simp3d Could not format ( ( `' _J ` x ) = <. z , y , n >. -> ( 2nd ` ( `' _J ` x ) ) = n ) : No typesetting found for |- ( ( `' _J ` x ) = <. z , y , n >. -> ( 2nd ` ( `' _J ` x ) ) = n ) with typecode |-
19 18 eqcomd Could not format ( ( `' _J ` x ) = <. z , y , n >. -> n = ( 2nd ` ( `' _J ` x ) ) ) : No typesetting found for |- ( ( `' _J ` x ) = <. z , y , n >. -> n = ( 2nd ` ( `' _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 -> n = ( 2nd ` ( `' _J ` x ) ) ) ) : No typesetting found for |- ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( ( _J ` <. z , y , n >. ) = x -> n = ( 2nd ` ( `' _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 >. ) -> n = ( 2nd ` ( `' _J ` x ) ) ) ) : No typesetting found for |- ( ( ( z e. On /\ y e. On /\ n e. 9o ) /\ x e. On ) -> ( x = ( _J ` <. z , y , n >. ) -> n = ( 2nd ` ( `' _J ` x ) ) ) ) with typecode |-
22 2 3 4 5 21 syl31anc Could not format ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> ( x = ( _J ` <. z , y , n >. ) -> n = ( 2nd ` ( `' _J ` x ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> ( x = ( _J ` <. z , y , n >. ) -> n = ( 2nd ` ( `' _J ` x ) ) ) ) with typecode |-
23 22 rexlimdva Could not format ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) -> ( E. y e. On x = ( _J ` <. z , y , n >. ) -> n = ( 2nd ` ( `' _J ` x ) ) ) ) : No typesetting found for |- ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) -> ( E. y e. On x = ( _J ` <. z , y , n >. ) -> n = ( 2nd ` ( `' _J ` x ) ) ) ) with typecode |-
24 23 rexlimdva Could not format ( ( x e. On /\ n e. 9o ) -> ( E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) -> n = ( 2nd ` ( `' _J ` x ) ) ) ) : No typesetting found for |- ( ( x e. On /\ n e. 9o ) -> ( E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) -> n = ( 2nd ` ( `' _J ` x ) ) ) ) with typecode |-
25 24 impr Could not format ( ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) -> n = ( 2nd ` ( `' _J ` x ) ) ) : No typesetting found for |- ( ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) -> n = ( 2nd ` ( `' _J ` x ) ) ) with typecode |-
26 1 25 jca Could not format ( ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) -> ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) ) : No typesetting found for |- ( ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) -> ( x e. On /\ n = ( 2nd ` ( `' _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 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 |-
30 28 29 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 |-
31 30 adantr Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( 2nd ` ( `' _J ` x ) ) e. 9o ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( 2nd ` ( `' _J ` x ) ) e. 9o ) with typecode |-
32 eleq1 Could not format ( n = ( 2nd ` ( `' _J ` x ) ) -> ( n e. 9o <-> ( 2nd ` ( `' _J ` x ) ) e. 9o ) ) : No typesetting found for |- ( n = ( 2nd ` ( `' _J ` x ) ) -> ( n e. 9o <-> ( 2nd ` ( `' _J ` x ) ) e. 9o ) ) with typecode |-
33 32 adantl Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( n e. 9o <-> ( 2nd ` ( `' _J ` x ) ) e. 9o ) ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( n e. 9o <-> ( 2nd ` ( `' _J ` x ) ) e. 9o ) ) with typecode |-
34 31 33 mpbird Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> n e. 9o ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> n e. 9o ) with typecode |-
35 oteq1 Could not format ( z = ( 1st ` ( 1st ` ( `' _J ` x ) ) ) -> <. z , y , n >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , n >. ) : No typesetting found for |- ( z = ( 1st ` ( 1st ` ( `' _J ` x ) ) ) -> <. z , y , n >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , n >. ) with typecode |-
36 35 eqeq2d Could not format ( z = ( 1st ` ( 1st ` ( `' _J ` x ) ) ) -> ( ( `' _J ` x ) = <. z , y , n >. <-> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , n >. ) ) : No typesetting found for |- ( z = ( 1st ` ( 1st ` ( `' _J ` x ) ) ) -> ( ( `' _J ` x ) = <. z , y , n >. <-> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , n >. ) ) with typecode |-
37 oteq2 Could not format ( y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , n >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. ) : No typesetting found for |- ( y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , n >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. ) with typecode |-
38 37 eqeq2d Could not format ( y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) -> ( ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , n >. <-> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. ) ) : No typesetting found for |- ( y = ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) -> ( ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , y , n >. <-> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. ) ) with typecode |-
39 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 |-
40 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 |-
41 28 39 40 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 |-
42 41 adantr Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) e. On ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( 1st ` ( 1st ` ( `' _J ` x ) ) ) e. On ) with typecode |-
43 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 |-
44 28 39 43 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 |-
45 44 adantr Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) e. On ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( 2nd ` ( 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 /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
49 oteq3 Could not format ( n = ( 2nd ` ( `' _J ` x ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( n = ( 2nd ` ( `' _J ` x ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
50 49 adantl Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( `' _J ` x ) ) >. ) with typecode |-
51 48 50 eqtr4d Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( `' _J ` x ) = <. ( 1st ` ( 1st ` ( `' _J ` x ) ) ) , ( 2nd ` ( 1st ` ( `' _J ` x ) ) ) , n >. ) with typecode |-
52 36 38 42 45 51 2rspcedvdw Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> E. z e. On E. y e. On ( `' _J ` x ) = <. z , y , n >. ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> E. z e. On E. y 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 /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> ( ( `' _J ` x ) = <. z , y , n >. -> x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) /\ y e. On ) -> ( ( `' _J ` x ) = <. z , y , n >. -> x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
56 55 reximdva Could not format ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) -> ( E. y e. On ( `' _J ` x ) = <. z , y , n >. -> E. y e. On x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( ( x e. On /\ n e. 9o ) /\ z e. On ) -> ( E. y e. On ( `' _J ` x ) = <. z , y , n >. -> E. y e. On x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
57 56 reximdva Could not format ( ( x e. On /\ n e. 9o ) -> ( E. z e. On E. y e. On ( `' _J ` x ) = <. z , y , n >. -> E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( x e. On /\ n e. 9o ) -> ( E. z e. On E. y e. On ( `' _J ` x ) = <. z , y , n >. -> E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
58 34 57 syldan Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( E. z e. On E. y e. On ( `' _J ` x ) = <. z , y , n >. -> E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( E. z e. On E. y e. On ( `' _J ` x ) = <. z , y , n >. -> E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) with typecode |-
59 52 58 mpd Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) with typecode |-
60 34 59 jca Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( n e. 9o /\ E. z e. On E. y 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 ⊢ ∅ ∈ 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. y e. On x = ( _J ` <. z , y , n >. ) -> x e. On ) : No typesetting found for |- ( E. y e. On x = ( _J ` <. z , y , n >. ) -> x e. On ) with typecode |-
68 67 rexlimivw Could not format ( E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) -> x e. On ) : No typesetting found for |- ( E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) -> x e. On ) with typecode |-
69 68 adantl Could not format ( ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) -> x e. On ) : No typesetting found for |- ( ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) -> x e. On ) with typecode |-
70 60 69 jccil Could not format ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) ) : No typesetting found for |- ( ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) -> ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) ) with typecode |-
71 26 70 impbii Could not format ( ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) <-> ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) ) : No typesetting found for |- ( ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) <-> ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) ) with typecode |-
72 71 opabbii Could not format { <. x , n >. | ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) } = { <. x , n >. | ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) } : No typesetting found for |- { <. x , n >. | ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) } = { <. x , n >. | ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) } with typecode |-
73 df-k3 Could not format _K3 = { <. x , n >. | ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) } : No typesetting found for |- _K3 = { <. x , n >. | ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) } with typecode |-
74 69 pm4.71ri Could not format ( ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) <-> ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) ) : No typesetting found for |- ( ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) <-> ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) ) with typecode |-
75 74 opabbii Could not format { <. x , n >. | ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) } = { <. x , n >. | ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) } : No typesetting found for |- { <. x , n >. | ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) } = { <. x , n >. | ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) } with typecode |-
76 73 75 eqtri Could not format _K3 = { <. x , n >. | ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) } : No typesetting found for |- _K3 = { <. x , n >. | ( x e. On /\ ( n e. 9o /\ E. z e. On E. y e. On x = ( _J ` <. z , y , n >. ) ) ) } with typecode |-
77 df-mpt Could not format ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) ) = { <. x , n >. | ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) } : No typesetting found for |- ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) ) = { <. x , n >. | ( x e. On /\ n = ( 2nd ` ( `' _J ` x ) ) ) } with typecode |-
78 72 76 77 3eqtr4i Could not format _K3 = ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) ) : No typesetting found for |- _K3 = ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) ) with typecode |-