Metamath Proof Explorer

Theorem edglnl

Description: The edges incident with a vertex N are the edges joining N with other vertices and the loops on N in a pseudograph. (Contributed by AV, 18-Dec-2021)

Ref Expression
Hypotheses edglnl.v 
|- V = ( Vtx ` G )
edglnl.e 
|- E = ( iEdg ` G )
Assertion edglnl 
|- ( ( G e. UPGraph /\ N e. V ) -> ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) = { i e. dom E | N e. ( E ` i ) } )

Proof

Step Hyp Ref Expression
1 edglnl.v 
 |-  V = ( Vtx ` G )
2 edglnl.e 
 |-  E = ( iEdg ` G )
3 iunrab 
 |-  U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } = { i e. dom E | E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) }
4 3 a1i 
 |-  ( ( G e. UPGraph /\ N e. V ) -> U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } = { i e. dom E | E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } )
5 4 uneq1d 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) = ( { i e. dom E | E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) )
6 unrab 
 |-  ( { i e. dom E | E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) = { i e. dom E | ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) }
7 simpl 
 |-  ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) -> N e. ( E ` i ) )
8 7 rexlimivw 
 |-  ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) -> N e. ( E ` i ) )
9 8 a1i 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) -> N e. ( E ` i ) ) )
10 snidg 
 |-  ( N e. V -> N e. { N } )
11 10 ad2antlr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> N e. { N } )
12 eleq2 
 |-  ( ( E ` i ) = { N } -> ( N e. ( E ` i ) <-> N e. { N } ) )
13 11 12 syl5ibrcom 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( ( E ` i ) = { N } -> N e. ( E ` i ) ) )
14 9 13 jaod 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) -> N e. ( E ` i ) ) )
15 upgruhgr 
 |-  ( G e. UPGraph -> G e. UHGraph )
16 2 uhgrfun 
 |-  ( G e. UHGraph -> Fun E )
17 15 16 syl 
 |-  ( G e. UPGraph -> Fun E )
18 17 adantr 
 |-  ( ( G e. UPGraph /\ N e. V ) -> Fun E )
19 2 iedgedg 
 |-  ( ( Fun E /\ i e. dom E ) -> ( E ` i ) e. ( Edg ` G ) )
20 18 19 sylan 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( E ` i ) e. ( Edg ` G ) )
21 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
22 1 21 upgredg 
 |-  ( ( G e. UPGraph /\ ( E ` i ) e. ( Edg ` G ) ) -> E. n e. V E. m e. V ( E ` i ) = { n , m } )
23 22 ex 
 |-  ( G e. UPGraph -> ( ( E ` i ) e. ( Edg ` G ) -> E. n e. V E. m e. V ( E ` i ) = { n , m } ) )
24 23 ad2antrr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( ( E ` i ) e. ( Edg ` G ) -> E. n e. V E. m e. V ( E ` i ) = { n , m } ) )
25 dfsn2 
 |-  { n } = { n , n }
26 25 eqcomi 
 |-  { n , n } = { n }
27 elsni 
 |-  ( N e. { n } -> N = n )
28 sneq 
 |-  ( N = n -> { N } = { n } )
29 28 eqcomd 
 |-  ( N = n -> { n } = { N } )
30 27 29 syl 
 |-  ( N e. { n } -> { n } = { N } )
31 26 30 syl5eq 
 |-  ( N e. { n } -> { n , n } = { N } )
32 31 26 eleq2s 
 |-  ( N e. { n , n } -> { n , n } = { N } )
33 preq2 
 |-  ( m = n -> { n , m } = { n , n } )
34 33 eleq2d 
 |-  ( m = n -> ( N e. { n , m } <-> N e. { n , n } ) )
35 33 eqeq1d 
 |-  ( m = n -> ( { n , m } = { N } <-> { n , n } = { N } ) )
36 34 35 imbi12d 
 |-  ( m = n -> ( ( N e. { n , m } -> { n , m } = { N } ) <-> ( N e. { n , n } -> { n , n } = { N } ) ) )
37 32 36 mpbiri 
 |-  ( m = n -> ( N e. { n , m } -> { n , m } = { N } ) )
38 37 imp 
 |-  ( ( m = n /\ N e. { n , m } ) -> { n , m } = { N } )
39 38 olcd 
 |-  ( ( m = n /\ N e. { n , m } ) -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) )
40 39 expcom 
 |-  ( N e. { n , m } -> ( m = n -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) ) )
41 40 3ad2ant3 
 |-  ( ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) -> ( m = n -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) ) )
42 41 com12 
 |-  ( m = n -> ( ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) ) )
43 simpr3 
 |-  ( ( m =/= n /\ ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) ) -> N e. { n , m } )
44 simpl 
 |-  ( ( m =/= n /\ ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) ) -> m =/= n )
45 44 necomd 
 |-  ( ( m =/= n /\ ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) ) -> n =/= m )
46 simpr2 
 |-  ( ( m =/= n /\ ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) ) -> ( n e. V /\ m e. V ) )
47 prproe 
 |-  ( ( N e. { n , m } /\ n =/= m /\ ( n e. V /\ m e. V ) ) -> E. v e. ( V \ { N } ) v e. { n , m } )
48 43 45 46 47 syl3anc 
 |-  ( ( m =/= n /\ ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) ) -> E. v e. ( V \ { N } ) v e. { n , m } )
49 r19.42v 
 |-  ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) <-> ( N e. { n , m } /\ E. v e. ( V \ { N } ) v e. { n , m } ) )
50 43 48 49 sylanbrc 
 |-  ( ( m =/= n /\ ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) ) -> E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) )
51 50 orcd 
 |-  ( ( m =/= n /\ ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) ) -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) )
52 51 ex 
 |-  ( m =/= n -> ( ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) ) )
53 42 52 pm2.61ine 
 |-  ( ( N e. V /\ ( n e. V /\ m e. V ) /\ N e. { n , m } ) -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) )
54 53 3exp 
 |-  ( N e. V -> ( ( n e. V /\ m e. V ) -> ( N e. { n , m } -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) ) ) )
55 54 ad2antlr 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( ( n e. V /\ m e. V ) -> ( N e. { n , m } -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) ) ) )
56 55 imp 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) /\ ( n e. V /\ m e. V ) ) -> ( N e. { n , m } -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) ) )
57 eleq2 
 |-  ( ( E ` i ) = { n , m } -> ( N e. ( E ` i ) <-> N e. { n , m } ) )
58 eleq2 
 |-  ( ( E ` i ) = { n , m } -> ( v e. ( E ` i ) <-> v e. { n , m } ) )
59 57 58 anbi12d 
 |-  ( ( E ` i ) = { n , m } -> ( ( N e. ( E ` i ) /\ v e. ( E ` i ) ) <-> ( N e. { n , m } /\ v e. { n , m } ) ) )
60 59 rexbidv 
 |-  ( ( E ` i ) = { n , m } -> ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) <-> E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) ) )
61 eqeq1 
 |-  ( ( E ` i ) = { n , m } -> ( ( E ` i ) = { N } <-> { n , m } = { N } ) )
62 60 61 orbi12d 
 |-  ( ( E ` i ) = { n , m } -> ( ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) <-> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) ) )
63 57 62 imbi12d 
 |-  ( ( E ` i ) = { n , m } -> ( ( N e. ( E ` i ) -> ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) ) <-> ( N e. { n , m } -> ( E. v e. ( V \ { N } ) ( N e. { n , m } /\ v e. { n , m } ) \/ { n , m } = { N } ) ) ) )
64 56 63 syl5ibrcom 
 |-  ( ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) /\ ( n e. V /\ m e. V ) ) -> ( ( E ` i ) = { n , m } -> ( N e. ( E ` i ) -> ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) ) ) )
65 64 rexlimdvva 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( E. n e. V E. m e. V ( E ` i ) = { n , m } -> ( N e. ( E ` i ) -> ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) ) ) )
66 24 65 syld 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( ( E ` i ) e. ( Edg ` G ) -> ( N e. ( E ` i ) -> ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) ) ) )
67 20 66 mpd 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( N e. ( E ` i ) -> ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) ) )
68 14 67 impbid 
 |-  ( ( ( G e. UPGraph /\ N e. V ) /\ i e. dom E ) -> ( ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) <-> N e. ( E ` i ) ) )
69 68 rabbidva 
 |-  ( ( G e. UPGraph /\ N e. V ) -> { i e. dom E | ( E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) \/ ( E ` i ) = { N } ) } = { i e. dom E | N e. ( E ` i ) } )
70 6 69 syl5eq 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( { i e. dom E | E. v e. ( V \ { N } ) ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) = { i e. dom E | N e. ( E ` i ) } )
71 5 70 eqtrd 
 |-  ( ( G e. UPGraph /\ N e. V ) -> ( U_ v e. ( V \ { N } ) { i e. dom E | ( N e. ( E ` i ) /\ v e. ( E ` i ) ) } u. { i e. dom E | ( E ` i ) = { N } } ) = { i e. dom E | N e. ( E ` i ) } )