Metamath Proof Explorer

Theorem gpgedgiov

Description: The edges of the generalized Petersen graph GPG(N,K) between an inside and an outside vertex. (Contributed by AV, 11-Nov-2025)

Ref Expression
Hypotheses gpgedgiov.j 
|- J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
gpgedgiov.i 
|- I = ( 0 ..^ N )
gpgedgiov.g 
|- G = ( N gPetersenGr K )
gpgedgiov.e 
|- E = ( Edg ` G )
Assertion gpgedgiov 
|- ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , X >. , <. 1 , Y >. } e. E <-> X = Y ) )

Proof

Step Hyp Ref Expression
1 gpgedgiov.j 
 |-  J = ( 1 ..^ ( |^ ` ( N / 2 ) ) )
2 gpgedgiov.i 
 |-  I = ( 0 ..^ N )
3 gpgedgiov.g 
 |-  G = ( N gPetersenGr K )
4 gpgedgiov.e 
 |-  E = ( Edg ` G )
5 simpll 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 1 , Y >. } e. E ) -> ( N e. ( ZZ>= ` 3 ) /\ K e. J ) )
6 c0ex 
 |-  0 e. _V
7 6 a1i 
 |-  ( Y e. I -> 0 e. _V )
8 7 anim1i 
 |-  ( ( Y e. I /\ X e. I ) -> ( 0 e. _V /\ X e. I ) )
9 8 ancoms 
 |-  ( ( X e. I /\ Y e. I ) -> ( 0 e. _V /\ X e. I ) )
10 op1stg 
 |-  ( ( 0 e. _V /\ X e. I ) -> ( 1st ` <. 0 , X >. ) = 0 )
11 9 10 syl 
 |-  ( ( X e. I /\ Y e. I ) -> ( 1st ` <. 0 , X >. ) = 0 )
12 11 ad2antlr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 1 , Y >. } e. E ) -> ( 1st ` <. 0 , X >. ) = 0 )
13 simpr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 1 , Y >. } e. E ) -> { <. 0 , X >. , <. 1 , Y >. } e. E )
14 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
15 1 3 14 4 gpgvtxedg0 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( 1st ` <. 0 , X >. ) = 0 /\ { <. 0 , X >. , <. 1 , Y >. } e. E ) -> ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) )
16 5 12 13 15 syl3anc 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ { <. 0 , X >. , <. 1 , Y >. } e. E ) -> ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) )
17 16 ex 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , X >. , <. 1 , Y >. } e. E -> ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) ) )
18 ovex 
 |-  ( ( X + 1 ) mod N ) e. _V
19 6 18 pm3.2i 
 |-  ( 0 e. _V /\ ( ( X + 1 ) mod N ) e. _V )
20 opthg2 
 |-  ( ( 0 e. _V /\ ( ( X + 1 ) mod N ) e. _V ) -> ( <. 1 , Y >. = <. 0 , ( ( X + 1 ) mod N ) >. <-> ( 1 = 0 /\ Y = ( ( X + 1 ) mod N ) ) ) )
21 19 20 mp1i 
 |-  ( ( X e. I /\ Y e. I ) -> ( <. 1 , Y >. = <. 0 , ( ( X + 1 ) mod N ) >. <-> ( 1 = 0 /\ Y = ( ( X + 1 ) mod N ) ) ) )
22 ax-1ne0 
 |-  1 =/= 0
23 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( Y = ( ( X + 1 ) mod N ) -> X = Y ) ) )
24 22 23 mpi 
 |-  ( 1 = 0 -> ( Y = ( ( X + 1 ) mod N ) -> X = Y ) )
25 24 imp 
 |-  ( ( 1 = 0 /\ Y = ( ( X + 1 ) mod N ) ) -> X = Y )
26 21 25 biimtrdi 
 |-  ( ( X e. I /\ Y e. I ) -> ( <. 1 , Y >. = <. 0 , ( ( X + 1 ) mod N ) >. -> X = Y ) )
27 1ex 
 |-  1 e. _V
28 27 a1i 
 |-  ( Y e. I -> 1 e. _V )
29 28 anim1i 
 |-  ( ( Y e. I /\ X e. I ) -> ( 1 e. _V /\ X e. I ) )
30 29 ancoms 
 |-  ( ( X e. I /\ Y e. I ) -> ( 1 e. _V /\ X e. I ) )
31 opthg2 
 |-  ( ( 1 e. _V /\ X e. I ) -> ( <. 1 , Y >. = <. 1 , X >. <-> ( 1 = 1 /\ Y = X ) ) )
32 30 31 syl 
 |-  ( ( X e. I /\ Y e. I ) -> ( <. 1 , Y >. = <. 1 , X >. <-> ( 1 = 1 /\ Y = X ) ) )
33 simpr 
 |-  ( ( 1 = 1 /\ Y = X ) -> Y = X )
34 33 eqcomd 
 |-  ( ( 1 = 1 /\ Y = X ) -> X = Y )
35 32 34 biimtrdi 
 |-  ( ( X e. I /\ Y e. I ) -> ( <. 1 , Y >. = <. 1 , X >. -> X = Y ) )
36 ovex 
 |-  ( ( X - 1 ) mod N ) e. _V
37 6 36 pm3.2i 
 |-  ( 0 e. _V /\ ( ( X - 1 ) mod N ) e. _V )
38 opthg2 
 |-  ( ( 0 e. _V /\ ( ( X - 1 ) mod N ) e. _V ) -> ( <. 1 , Y >. = <. 0 , ( ( X - 1 ) mod N ) >. <-> ( 1 = 0 /\ Y = ( ( X - 1 ) mod N ) ) ) )
39 37 38 mp1i 
 |-  ( ( X e. I /\ Y e. I ) -> ( <. 1 , Y >. = <. 0 , ( ( X - 1 ) mod N ) >. <-> ( 1 = 0 /\ Y = ( ( X - 1 ) mod N ) ) ) )
40 eqneqall 
 |-  ( 1 = 0 -> ( 1 =/= 0 -> ( Y = ( ( X - 1 ) mod N ) -> X = Y ) ) )
41 22 40 mpi 
 |-  ( 1 = 0 -> ( Y = ( ( X - 1 ) mod N ) -> X = Y ) )
42 41 imp 
 |-  ( ( 1 = 0 /\ Y = ( ( X - 1 ) mod N ) ) -> X = Y )
43 39 42 biimtrdi 
 |-  ( ( X e. I /\ Y e. I ) -> ( <. 1 , Y >. = <. 0 , ( ( X - 1 ) mod N ) >. -> X = Y ) )
44 26 35 43 3jaod 
 |-  ( ( X e. I /\ Y e. I ) -> ( ( <. 1 , Y >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , X >. \/ <. 1 , Y >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) )
45 op2ndg 
 |-  ( ( 0 e. _V /\ X e. I ) -> ( 2nd ` <. 0 , X >. ) = X )
46 9 45 syl 
 |-  ( ( X e. I /\ Y e. I ) -> ( 2nd ` <. 0 , X >. ) = X )
47 oveq1 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( 2nd ` <. 0 , X >. ) + 1 ) = ( X + 1 ) )
48 47 oveq1d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) = ( ( X + 1 ) mod N ) )
49 48 opeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. = <. 0 , ( ( X + 1 ) mod N ) >. )
50 49 eqeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. <-> <. 1 , Y >. = <. 0 , ( ( X + 1 ) mod N ) >. ) )
51 opeq2 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> <. 1 , ( 2nd ` <. 0 , X >. ) >. = <. 1 , X >. )
52 51 eqeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( <. 1 , Y >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. <-> <. 1 , Y >. = <. 1 , X >. ) )
53 oveq1 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( 2nd ` <. 0 , X >. ) - 1 ) = ( X - 1 ) )
54 53 oveq1d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) = ( ( X - 1 ) mod N ) )
55 54 opeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. = <. 0 , ( ( X - 1 ) mod N ) >. )
56 55 eqeq2d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. <-> <. 1 , Y >. = <. 0 , ( ( X - 1 ) mod N ) >. ) )
57 50 52 56 3orbi123d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) <-> ( <. 1 , Y >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , X >. \/ <. 1 , Y >. = <. 0 , ( ( X - 1 ) mod N ) >. ) ) )
58 57 imbi1d 
 |-  ( ( 2nd ` <. 0 , X >. ) = X -> ( ( ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> X = Y ) <-> ( ( <. 1 , Y >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , X >. \/ <. 1 , Y >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) ) )
59 46 58 syl 
 |-  ( ( X e. I /\ Y e. I ) -> ( ( ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> X = Y ) <-> ( ( <. 1 , Y >. = <. 0 , ( ( X + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , X >. \/ <. 1 , Y >. = <. 0 , ( ( X - 1 ) mod N ) >. ) -> X = Y ) ) )
60 44 59 mpbird 
 |-  ( ( X e. I /\ Y e. I ) -> ( ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> X = Y ) )
61 60 adantl 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( ( <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) + 1 ) mod N ) >. \/ <. 1 , Y >. = <. 1 , ( 2nd ` <. 0 , X >. ) >. \/ <. 1 , Y >. = <. 0 , ( ( ( 2nd ` <. 0 , X >. ) - 1 ) mod N ) >. ) -> X = Y ) )
62 17 61 syld 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , X >. , <. 1 , Y >. } e. E -> X = Y ) )
63 simpr 
 |-  ( ( X e. I /\ Y e. I ) -> Y e. I )
64 63 ad2antlr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ X = Y ) -> Y e. I )
65 opeq2 
 |-  ( x = Y -> <. 0 , x >. = <. 0 , Y >. )
66 oveq1 
 |-  ( x = Y -> ( x + 1 ) = ( Y + 1 ) )
67 66 oveq1d 
 |-  ( x = Y -> ( ( x + 1 ) mod N ) = ( ( Y + 1 ) mod N ) )
68 67 opeq2d 
 |-  ( x = Y -> <. 0 , ( ( x + 1 ) mod N ) >. = <. 0 , ( ( Y + 1 ) mod N ) >. )
69 65 68 preq12d 
 |-  ( x = Y -> { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } = { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } )
70 69 eqeq2d 
 |-  ( x = Y -> ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } <-> { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } ) )
71 opeq2 
 |-  ( x = Y -> <. 1 , x >. = <. 1 , Y >. )
72 65 71 preq12d 
 |-  ( x = Y -> { <. 0 , x >. , <. 1 , x >. } = { <. 0 , Y >. , <. 1 , Y >. } )
73 72 eqeq2d 
 |-  ( x = Y -> ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 1 , x >. } <-> { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 1 , Y >. } ) )
74 oveq1 
 |-  ( x = Y -> ( x + K ) = ( Y + K ) )
75 74 oveq1d 
 |-  ( x = Y -> ( ( x + K ) mod N ) = ( ( Y + K ) mod N ) )
76 75 opeq2d 
 |-  ( x = Y -> <. 1 , ( ( x + K ) mod N ) >. = <. 1 , ( ( Y + K ) mod N ) >. )
77 71 76 preq12d 
 |-  ( x = Y -> { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } = { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } )
78 77 eqeq2d 
 |-  ( x = Y -> ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } <-> { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } ) )
79 70 73 78 3orbi123d 
 |-  ( x = Y -> ( ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 1 , Y >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } ) ) )
80 79 adantl 
 |-  ( ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ X = Y ) /\ x = Y ) -> ( ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) <-> ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 1 , Y >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } ) ) )
81 eqidd 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ X = Y ) -> { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 1 , Y >. } )
82 81 3mix2d 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ X = Y ) -> ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 0 , ( ( Y + 1 ) mod N ) >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 1 , Y >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , Y >. , <. 1 , ( ( Y + K ) mod N ) >. } ) )
83 64 80 82 rspcedvd 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ X = Y ) -> E. x e. I ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) )
84 2 1 3 4 gpgedgel 
 |-  ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) -> ( { <. 0 , Y >. , <. 1 , Y >. } e. E <-> E. x e. I ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
85 84 ad2antrr 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ X = Y ) -> ( { <. 0 , Y >. , <. 1 , Y >. } e. E <-> E. x e. I ( { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 0 , ( ( x + 1 ) mod N ) >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 0 , x >. , <. 1 , x >. } \/ { <. 0 , Y >. , <. 1 , Y >. } = { <. 1 , x >. , <. 1 , ( ( x + K ) mod N ) >. } ) ) )
86 83 85 mpbird 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ X = Y ) -> { <. 0 , Y >. , <. 1 , Y >. } e. E )
87 opeq2 
 |-  ( X = Y -> <. 0 , X >. = <. 0 , Y >. )
88 87 preq1d 
 |-  ( X = Y -> { <. 0 , X >. , <. 1 , Y >. } = { <. 0 , Y >. , <. 1 , Y >. } )
89 88 eleq1d 
 |-  ( X = Y -> ( { <. 0 , X >. , <. 1 , Y >. } e. E <-> { <. 0 , Y >. , <. 1 , Y >. } e. E ) )
90 89 adantl 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ X = Y ) -> ( { <. 0 , X >. , <. 1 , Y >. } e. E <-> { <. 0 , Y >. , <. 1 , Y >. } e. E ) )
91 86 90 mpbird 
 |-  ( ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) /\ X = Y ) -> { <. 0 , X >. , <. 1 , Y >. } e. E )
92 91 ex 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( X = Y -> { <. 0 , X >. , <. 1 , Y >. } e. E ) )
93 62 92 impbid 
 |-  ( ( ( N e. ( ZZ>= ` 3 ) /\ K e. J ) /\ ( X e. I /\ Y e. I ) ) -> ( { <. 0 , X >. , <. 1 , Y >. } e. E <-> X = Y ) )