Metamath Proof Explorer

Theorem gpgprismgr4cycllem8

Description: Lemma 8 for gpgprismgr4cycl0 . (Contributed by AV, 2-Nov-2025)

Ref Expression
Hypotheses gpgprismgr4cycl.p 
|- P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
gpgprismgr4cycl.f 
|- F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
gpgprismgr4cycl.g 
|- G = ( N gPetersenGr 1 )
Assertion gpgprismgr4cycllem8 
|- ( N e. ( ZZ>= ` 3 ) -> F e. Word dom ( iEdg ` G ) )

Proof

Step Hyp Ref Expression
1 gpgprismgr4cycl.p 
 |-  P = <" <. 0 , 0 >. <. 0 , 1 >. <. 1 , 1 >. <. 1 , 0 >. <. 0 , 0 >. ">
2 gpgprismgr4cycl.f 
 |-  F = <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } ">
3 gpgprismgr4cycl.g 
 |-  G = ( N gPetersenGr 1 )
4 df-s4 
 |-  <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } { <. 1 , 0 >. , <. 0 , 0 >. } "> = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } "> ++ <" { <. 1 , 0 >. , <. 0 , 0 >. } "> )
5 2 4 eqtri 
 |-  F = ( <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } "> ++ <" { <. 1 , 0 >. , <. 0 , 0 >. } "> )
6 gpgprismgriedgdmss 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) )
7 unss 
 |-  ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) <-> ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) )
8 prex 
 |-  { <. 0 , 0 >. , <. 0 , 1 >. } e. _V
9 prex 
 |-  { <. 0 , 0 >. , <. 1 , 0 >. } e. _V
10 8 9 prss 
 |-  ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) <-> { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) )
11 3 eqcomi 
 |-  ( N gPetersenGr 1 ) = G
12 11 fveq2i 
 |-  ( iEdg ` ( N gPetersenGr 1 ) ) = ( iEdg ` G )
13 12 dmeqi 
 |-  dom ( iEdg ` ( N gPetersenGr 1 ) ) = dom ( iEdg ` G )
14 13 eleq2i 
 |-  ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) )
15 14 biimpi 
 |-  ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) )
16 15 adantr 
 |-  ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) )
17 10 16 sylbir 
 |-  ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) )
18 17 adantr 
 |-  ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) )
19 7 18 sylbir 
 |-  ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) )
20 6 19 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) )
21 prex 
 |-  { <. 1 , 1 >. , <. 0 , 1 >. } e. _V
22 prex 
 |-  { <. 1 , 1 >. , <. 1 , 0 >. } e. _V
23 21 22 prss 
 |-  ( ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) <-> { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) )
24 prcom 
 |-  { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. }
25 24 13 eleq12i 
 |-  ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
26 25 biimpi 
 |-  ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
27 26 adantr 
 |-  ( ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
28 23 27 sylbir 
 |-  ( { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
29 28 adantl 
 |-  ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
30 7 29 sylbir 
 |-  ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
31 6 30 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
32 13 eleq2i 
 |-  ( { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
33 32 biimpi 
 |-  ( { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
34 33 adantl 
 |-  ( ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
35 23 34 sylbir 
 |-  ( { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
36 35 adantl 
 |-  ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
37 7 36 sylbir 
 |-  ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
38 6 37 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
39 20 31 38 s3cld 
 |-  ( N e. ( ZZ>= ` 3 ) -> <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } "> e. Word dom ( iEdg ` G ) )
40 simpr 
 |-  ( ( { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) )
41 10 40 sylbir 
 |-  ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) )
42 prcom 
 |-  { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. }
43 3 fveq2i 
 |-  ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) )
44 43 dmeqi 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` ( N gPetersenGr 1 ) )
45 41 42 44 3eltr4g 
 |-  ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) )
46 45 adantr 
 |-  ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) /\ { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) )
47 7 46 sylbir 
 |-  ( ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } u. { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } ) C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) )
48 6 47 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) )
49 5 39 48 cats1cld 
 |-  ( N e. ( ZZ>= ` 3 ) -> F e. Word dom ( iEdg ` G ) )