Metamath Proof Explorer

Theorem uspgropssxp

Description: The set G of "simple pseudographs" for a fixed set V of vertices is a subset of a Cartesian product. For more details about the class G of all "simple pseudographs" see comments on uspgrbisymrel . (Contributed by AV, 24-Nov-2021)

Ref Expression
Hypotheses uspgrsprf.p 
|- P = ~P ( Pairs ` V )
uspgrsprf.g 
|- G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
Assertion uspgropssxp 
|- ( V e. W -> G C_ ( W X. P ) )

Proof

Step Hyp Ref Expression
1 uspgrsprf.p 
 |-  P = ~P ( Pairs ` V )
2 uspgrsprf.g 
 |-  G = { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) }
3 eleq1 
 |-  ( V = v -> ( V e. W <-> v e. W ) )
4 3 eqcoms 
 |-  ( v = V -> ( V e. W <-> v e. W ) )
5 4 adantr 
 |-  ( ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) -> ( V e. W <-> v e. W ) )
6 5 biimpac 
 |-  ( ( V e. W /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> v e. W )
7 uspgrupgr 
 |-  ( q e. USPGraph -> q e. UPGraph )
8 upgredgssspr 
 |-  ( q e. UPGraph -> ( Edg ` q ) C_ ( Pairs ` ( Vtx ` q ) ) )
9 7 8 syl 
 |-  ( q e. USPGraph -> ( Edg ` q ) C_ ( Pairs ` ( Vtx ` q ) ) )
10 9 3ad2ant1 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> ( Edg ` q ) C_ ( Pairs ` ( Vtx ` q ) ) )
11 simp2l 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> ( Vtx ` q ) = v )
12 simp3 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> v = V )
13 11 12 eqtrd 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> ( Vtx ` q ) = V )
14 13 fveq2d 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> ( Pairs ` ( Vtx ` q ) ) = ( Pairs ` V ) )
15 10 14 sseqtrd 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> ( Edg ` q ) C_ ( Pairs ` V ) )
16 fvex 
 |-  ( Edg ` q ) e. _V
17 16 elpw 
 |-  ( ( Edg ` q ) e. ~P ( Pairs ` V ) <-> ( Edg ` q ) C_ ( Pairs ` V ) )
18 15 17 sylibr 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> ( Edg ` q ) e. ~P ( Pairs ` V ) )
19 simpr 
 |-  ( ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) -> ( Edg ` q ) = e )
20 19 eqcomd 
 |-  ( ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) -> e = ( Edg ` q ) )
21 20 3ad2ant2 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> e = ( Edg ` q ) )
22 1 a1i 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> P = ~P ( Pairs ` V ) )
23 18 21 22 3eltr4d 
 |-  ( ( q e. USPGraph /\ ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) /\ v = V ) -> e e. P )
24 23 3exp 
 |-  ( q e. USPGraph -> ( ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) -> ( v = V -> e e. P ) ) )
25 24 rexlimiv 
 |-  ( E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) -> ( v = V -> e e. P ) )
26 25 impcom 
 |-  ( ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) -> e e. P )
27 26 adantl 
 |-  ( ( V e. W /\ ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) ) -> e e. P )
28 6 27 opabssxpd 
 |-  ( V e. W -> { <. v , e >. | ( v = V /\ E. q e. USPGraph ( ( Vtx ` q ) = v /\ ( Edg ` q ) = e ) ) } C_ ( W X. P ) )
29 2 28 eqsstrid 
 |-  ( V e. W -> G C_ ( W X. P ) )