Step |
Hyp |
Ref |
Expression |
1 |
|
konigsberg.v |
β’ π = ( 0 ... 3 ) |
2 |
|
konigsberg.e |
β’ πΈ = β¨β { 0 , 1 } { 0 , 2 } { 0 , 3 } { 1 , 2 } { 1 , 2 } { 2 , 3 } { 2 , 3 } ββ© |
3 |
|
konigsberg.g |
β’ πΊ = β¨ π , πΈ β© |
4 |
1 2 3
|
konigsbergssiedgwpr |
β’ ( ( π΄ β Word V β§ π΅ β Word V β§ πΈ = ( π΄ ++ π΅ ) ) β π΄ β Word { π₯ β π« π β£ ( β― β π₯ ) = 2 } ) |
5 |
|
wrdf |
β’ ( π΄ β Word { π₯ β π« π β£ ( β― β π₯ ) = 2 } β π΄ : ( 0 ..^ ( β― β π΄ ) ) βΆ { π₯ β π« π β£ ( β― β π₯ ) = 2 } ) |
6 |
|
prprrab |
β’ { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) = 2 } = { π₯ β π« π β£ ( β― β π₯ ) = 2 } |
7 |
|
2re |
β’ 2 β β |
8 |
7
|
eqlei2 |
β’ ( ( β― β π₯ ) = 2 β ( β― β π₯ ) β€ 2 ) |
9 |
8
|
a1i |
β’ ( π₯ β ( π« π β { β
} ) β ( ( β― β π₯ ) = 2 β ( β― β π₯ ) β€ 2 ) ) |
10 |
9
|
ss2rabi |
β’ { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) = 2 } β { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) β€ 2 } |
11 |
6 10
|
eqsstrri |
β’ { π₯ β π« π β£ ( β― β π₯ ) = 2 } β { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) β€ 2 } |
12 |
|
fss |
β’ ( ( π΄ : ( 0 ..^ ( β― β π΄ ) ) βΆ { π₯ β π« π β£ ( β― β π₯ ) = 2 } β§ { π₯ β π« π β£ ( β― β π₯ ) = 2 } β { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) β€ 2 } ) β π΄ : ( 0 ..^ ( β― β π΄ ) ) βΆ { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) β€ 2 } ) |
13 |
11 12
|
mpan2 |
β’ ( π΄ : ( 0 ..^ ( β― β π΄ ) ) βΆ { π₯ β π« π β£ ( β― β π₯ ) = 2 } β π΄ : ( 0 ..^ ( β― β π΄ ) ) βΆ { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) β€ 2 } ) |
14 |
|
iswrdb |
β’ ( π΄ β Word { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) β€ 2 } β π΄ : ( 0 ..^ ( β― β π΄ ) ) βΆ { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) β€ 2 } ) |
15 |
13 14
|
sylibr |
β’ ( π΄ : ( 0 ..^ ( β― β π΄ ) ) βΆ { π₯ β π« π β£ ( β― β π₯ ) = 2 } β π΄ β Word { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) β€ 2 } ) |
16 |
4 5 15
|
3syl |
β’ ( ( π΄ β Word V β§ π΅ β Word V β§ πΈ = ( π΄ ++ π΅ ) ) β π΄ β Word { π₯ β ( π« π β { β
} ) β£ ( β― β π₯ ) β€ 2 } ) |