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 birani 
 |-  ( ( { <. 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 ) )
16 10 15 sylbir 
 |-  ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) )
17 16 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 ) )
18 7 17 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 ) )
19 6 18 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 0 >. , <. 0 , 1 >. } e. dom ( iEdg ` G ) )
20 prex 
 |-  { <. 1 , 1 >. , <. 0 , 1 >. } e. _V
21 prex 
 |-  { <. 1 , 1 >. , <. 1 , 0 >. } e. _V
22 20 21 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 ) ) )
23 prcom 
 |-  { <. 1 , 1 >. , <. 0 , 1 >. } = { <. 0 , 1 >. , <. 1 , 1 >. }
24 23 13 eleq12i 
 |-  ( { <. 1 , 1 >. , <. 0 , 1 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
25 24 birani 
 |-  ( ( { <. 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 ) )
26 22 25 sylbir 
 |-  ( { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
27 26 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 ) )
28 7 27 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 ) )
29 6 28 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 0 , 1 >. , <. 1 , 1 >. } e. dom ( iEdg ` G ) )
30 13 eleq2i 
 |-  ( { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` ( N gPetersenGr 1 ) ) <-> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
31 30 bilani 
 |-  ( ( { <. 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 ) )
32 22 31 sylbir 
 |-  ( { { <. 1 , 1 >. , <. 0 , 1 >. } , { <. 1 , 1 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
33 32 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 ) )
34 7 33 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 ) )
35 6 34 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 1 >. , <. 1 , 0 >. } e. dom ( iEdg ` G ) )
36 19 29 35 s3cld 
 |-  ( N e. ( ZZ>= ` 3 ) -> <" { <. 0 , 0 >. , <. 0 , 1 >. } { <. 0 , 1 >. , <. 1 , 1 >. } { <. 1 , 1 >. , <. 1 , 0 >. } "> e. Word dom ( iEdg ` G ) )
37 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 ) ) )
38 10 37 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 ) ) )
39 prcom 
 |-  { <. 1 , 0 >. , <. 0 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. }
40 3 fveq2i 
 |-  ( iEdg ` G ) = ( iEdg ` ( N gPetersenGr 1 ) )
41 40 dmeqi 
 |-  dom ( iEdg ` G ) = dom ( iEdg ` ( N gPetersenGr 1 ) )
42 38 39 41 3eltr4g 
 |-  ( { { <. 0 , 0 >. , <. 0 , 1 >. } , { <. 0 , 0 >. , <. 1 , 0 >. } } C_ dom ( iEdg ` ( N gPetersenGr 1 ) ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) )
43 42 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 ) )
44 7 43 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 ) )
45 6 44 syl 
 |-  ( N e. ( ZZ>= ` 3 ) -> { <. 1 , 0 >. , <. 0 , 0 >. } e. dom ( iEdg ` G ) )
46 5 36 45 cats1cld 
 |-  ( N e. ( ZZ>= ` 3 ) -> F e. Word dom ( iEdg ` G ) )