Metamath Proof Explorer

Theorem dfk32

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

Ref Expression
Assertion dfk32 
|- _K3 = ( x e. On |-> ( 2nd ` ( `' _J ` x ) ) )

Proof

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