Metamath Proof Explorer

Theorem uhgr2edg

Description: If a vertex is adjacent to two different vertices in a hypergraph, there are more than one edges starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 11-Feb-2021)

Ref Expression
Hypotheses usgrf1oedg.i 
|- I = ( iEdg ` G )
usgrf1oedg.e 
|- E = ( Edg ` G )
uhgr2edg.v 
|- V = ( Vtx ` G )
Assertion uhgr2edg 
|- ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )

Proof

Step Hyp Ref Expression
1 usgrf1oedg.i 
 |-  I = ( iEdg ` G )
2 usgrf1oedg.e 
 |-  E = ( Edg ` G )
3 uhgr2edg.v 
 |-  V = ( Vtx ` G )
4 simp1l 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> G e. UHGraph )
5 simp1r 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> A =/= B )
6 simp23 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> N e. V )
7 simp21 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> A e. V )
8 3simpc 
 |-  ( ( A e. V /\ B e. V /\ N e. V ) -> ( B e. V /\ N e. V ) )
9 8 3ad2ant2 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> ( B e. V /\ N e. V ) )
10 6 7 9 jca31 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) )
11 4 5 10 jca31 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) )
12 simp3 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> ( { N , A } e. E /\ { B , N } e. E ) )
13 2 a1i 
 |-  ( G e. UHGraph -> E = ( Edg ` G ) )
14 edgval 
 |-  ( Edg ` G ) = ran ( iEdg ` G )
15 14 a1i 
 |-  ( G e. UHGraph -> ( Edg ` G ) = ran ( iEdg ` G ) )
16 1 eqcomi 
 |-  ( iEdg ` G ) = I
17 16 a1i 
 |-  ( G e. UHGraph -> ( iEdg ` G ) = I )
18 17 rneqd 
 |-  ( G e. UHGraph -> ran ( iEdg ` G ) = ran I )
19 13 15 18 3eqtrd 
 |-  ( G e. UHGraph -> E = ran I )
20 19 eleq2d 
 |-  ( G e. UHGraph -> ( { N , A } e. E <-> { N , A } e. ran I ) )
21 19 eleq2d 
 |-  ( G e. UHGraph -> ( { B , N } e. E <-> { B , N } e. ran I ) )
22 20 21 anbi12d 
 |-  ( G e. UHGraph -> ( ( { N , A } e. E /\ { B , N } e. E ) <-> ( { N , A } e. ran I /\ { B , N } e. ran I ) ) )
23 1 uhgrfun 
 |-  ( G e. UHGraph -> Fun I )
24 23 funfnd 
 |-  ( G e. UHGraph -> I Fn dom I )
25 fvelrnb 
 |-  ( I Fn dom I -> ( { N , A } e. ran I <-> E. x e. dom I ( I ` x ) = { N , A } ) )
26 fvelrnb 
 |-  ( I Fn dom I -> ( { B , N } e. ran I <-> E. y e. dom I ( I ` y ) = { B , N } ) )
27 25 26 anbi12d 
 |-  ( I Fn dom I -> ( ( { N , A } e. ran I /\ { B , N } e. ran I ) <-> ( E. x e. dom I ( I ` x ) = { N , A } /\ E. y e. dom I ( I ` y ) = { B , N } ) ) )
28 24 27 syl 
 |-  ( G e. UHGraph -> ( ( { N , A } e. ran I /\ { B , N } e. ran I ) <-> ( E. x e. dom I ( I ` x ) = { N , A } /\ E. y e. dom I ( I ` y ) = { B , N } ) ) )
29 22 28 bitrd 
 |-  ( G e. UHGraph -> ( ( { N , A } e. E /\ { B , N } e. E ) <-> ( E. x e. dom I ( I ` x ) = { N , A } /\ E. y e. dom I ( I ` y ) = { B , N } ) ) )
30 29 ad2antrr 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> ( ( { N , A } e. E /\ { B , N } e. E ) <-> ( E. x e. dom I ( I ` x ) = { N , A } /\ E. y e. dom I ( I ` y ) = { B , N } ) ) )
31 reeanv 
 |-  ( E. x e. dom I E. y e. dom I ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) <-> ( E. x e. dom I ( I ` x ) = { N , A } /\ E. y e. dom I ( I ` y ) = { B , N } ) )
32 fveqeq2 
 |-  ( x = y -> ( ( I ` x ) = { N , A } <-> ( I ` y ) = { N , A } ) )
33 32 anbi1d 
 |-  ( x = y -> ( ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) <-> ( ( I ` y ) = { N , A } /\ ( I ` y ) = { B , N } ) ) )
34 eqtr2 
 |-  ( ( ( I ` y ) = { N , A } /\ ( I ` y ) = { B , N } ) -> { N , A } = { B , N } )
35 prcom 
 |-  { B , N } = { N , B }
36 35 eqeq2i 
 |-  ( { N , A } = { B , N } <-> { N , A } = { N , B } )
37 preq12bg 
 |-  ( ( ( N e. V /\ A e. V ) /\ ( N e. V /\ B e. V ) ) -> ( { N , A } = { N , B } <-> ( ( N = N /\ A = B ) \/ ( N = B /\ A = N ) ) ) )
38 37 ancom2s 
 |-  ( ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) -> ( { N , A } = { N , B } <-> ( ( N = N /\ A = B ) \/ ( N = B /\ A = N ) ) ) )
39 eqneqall 
 |-  ( A = B -> ( A =/= B -> x =/= y ) )
40 39 adantl 
 |-  ( ( N = N /\ A = B ) -> ( A =/= B -> x =/= y ) )
41 eqtr 
 |-  ( ( A = N /\ N = B ) -> A = B )
42 41 ancoms 
 |-  ( ( N = B /\ A = N ) -> A = B )
43 42 39 syl 
 |-  ( ( N = B /\ A = N ) -> ( A =/= B -> x =/= y ) )
44 40 43 jaoi 
 |-  ( ( ( N = N /\ A = B ) \/ ( N = B /\ A = N ) ) -> ( A =/= B -> x =/= y ) )
45 44 adantld 
 |-  ( ( ( N = N /\ A = B ) \/ ( N = B /\ A = N ) ) -> ( ( G e. UHGraph /\ A =/= B ) -> x =/= y ) )
46 38 45 biimtrdi 
 |-  ( ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) -> ( { N , A } = { N , B } -> ( ( G e. UHGraph /\ A =/= B ) -> x =/= y ) ) )
47 46 com3l 
 |-  ( { N , A } = { N , B } -> ( ( G e. UHGraph /\ A =/= B ) -> ( ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) -> x =/= y ) ) )
48 47 impd 
 |-  ( { N , A } = { N , B } -> ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> x =/= y ) )
49 36 48 sylbi 
 |-  ( { N , A } = { B , N } -> ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> x =/= y ) )
50 34 49 syl 
 |-  ( ( ( I ` y ) = { N , A } /\ ( I ` y ) = { B , N } ) -> ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> x =/= y ) )
51 33 50 biimtrdi 
 |-  ( x = y -> ( ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) -> ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> x =/= y ) ) )
52 51 impcomd 
 |-  ( x = y -> ( ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) /\ ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) ) -> x =/= y ) )
53 ax-1 
 |-  ( x =/= y -> ( ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) /\ ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) ) -> x =/= y ) )
54 52 53 pm2.61ine 
 |-  ( ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) /\ ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) ) -> x =/= y )
55 prid1g 
 |-  ( N e. V -> N e. { N , A } )
56 55 ad2antrr 
 |-  ( ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) -> N e. { N , A } )
57 56 adantl 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> N e. { N , A } )
58 eleq2 
 |-  ( ( I ` x ) = { N , A } -> ( N e. ( I ` x ) <-> N e. { N , A } ) )
59 57 58 imbitrrid 
 |-  ( ( I ` x ) = { N , A } -> ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> N e. ( I ` x ) ) )
60 59 adantr 
 |-  ( ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) -> ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> N e. ( I ` x ) ) )
61 60 impcom 
 |-  ( ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) /\ ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) ) -> N e. ( I ` x ) )
62 prid2g 
 |-  ( N e. V -> N e. { B , N } )
63 62 ad2antrr 
 |-  ( ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) -> N e. { B , N } )
64 63 adantl 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> N e. { B , N } )
65 eleq2 
 |-  ( ( I ` y ) = { B , N } -> ( N e. ( I ` y ) <-> N e. { B , N } ) )
66 64 65 imbitrrid 
 |-  ( ( I ` y ) = { B , N } -> ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> N e. ( I ` y ) ) )
67 66 adantl 
 |-  ( ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) -> ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> N e. ( I ` y ) ) )
68 67 impcom 
 |-  ( ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) /\ ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) ) -> N e. ( I ` y ) )
69 54 61 68 3jca 
 |-  ( ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) /\ ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) ) -> ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )
70 69 ex 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> ( ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) -> ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) ) )
71 70 reximdv 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> ( E. y e. dom I ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) -> E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) ) )
72 71 reximdv 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> ( E. x e. dom I E. y e. dom I ( ( I ` x ) = { N , A } /\ ( I ` y ) = { B , N } ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) ) )
73 31 72 biimtrrid 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> ( ( E. x e. dom I ( I ` x ) = { N , A } /\ E. y e. dom I ( I ` y ) = { B , N } ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) ) )
74 30 73 sylbid 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( ( N e. V /\ A e. V ) /\ ( B e. V /\ N e. V ) ) ) -> ( ( { N , A } e. E /\ { B , N } e. E ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) ) )
75 11 12 74 sylc 
 |-  ( ( ( G e. UHGraph /\ A =/= B ) /\ ( A e. V /\ B e. V /\ N e. V ) /\ ( { N , A } e. E /\ { B , N } e. E ) ) -> E. x e. dom I E. y e. dom I ( x =/= y /\ N e. ( I ` x ) /\ N e. ( I ` y ) ) )