Metamath Proof Explorer

Theorem upgrex

Description: An edge is an unordered pair of vertices. (Contributed by Mario Carneiro, 11-Mar-2015) (Revised by AV, 10-Oct-2020)

Ref Expression
Hypotheses isupgr.v 
|- V = ( Vtx ` G )
isupgr.e 
|- E = ( iEdg ` G )
Assertion upgrex 
|- ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> E. x e. V E. y e. V ( E ` F ) = { x , y } )

Proof

Step Hyp Ref Expression
1 isupgr.v 
 |-  V = ( Vtx ` G )
2 isupgr.e 
 |-  E = ( iEdg ` G )
3 1 2 upgrn0 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) =/= (/) )
4 n0 
 |-  ( ( E ` F ) =/= (/) <-> E. x x e. ( E ` F ) )
5 3 4 sylib 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> E. x x e. ( E ` F ) )
6 simp1 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> G e. UPGraph )
7 fndm 
 |-  ( E Fn A -> dom E = A )
8 7 eqcomd 
 |-  ( E Fn A -> A = dom E )
9 8 eleq2d 
 |-  ( E Fn A -> ( F e. A <-> F e. dom E ) )
10 9 biimpd 
 |-  ( E Fn A -> ( F e. A -> F e. dom E ) )
11 10 a1i 
 |-  ( G e. UPGraph -> ( E Fn A -> ( F e. A -> F e. dom E ) ) )
12 11 3imp 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> F e. dom E )
13 1 2 upgrss 
 |-  ( ( G e. UPGraph /\ F e. dom E ) -> ( E ` F ) C_ V )
14 6 12 13 syl2anc 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) C_ V )
15 14 sselda 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> x e. V )
16 15 adantr 
 |-  ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> x e. V )
17 simpr 
 |-  ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> ( ( E ` F ) \ { x } ) = (/) )
18 ssdif0 
 |-  ( ( E ` F ) C_ { x } <-> ( ( E ` F ) \ { x } ) = (/) )
19 17 18 sylibr 
 |-  ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> ( E ` F ) C_ { x } )
20 simpr 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> x e. ( E ` F ) )
21 20 snssd 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> { x } C_ ( E ` F ) )
22 21 adantr 
 |-  ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> { x } C_ ( E ` F ) )
23 19 22 eqssd 
 |-  ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> ( E ` F ) = { x } )
24 preq2 
 |-  ( y = x -> { x , y } = { x , x } )
25 dfsn2 
 |-  { x } = { x , x }
26 24 25 eqtr4di 
 |-  ( y = x -> { x , y } = { x } )
27 26 rspceeqv 
 |-  ( ( x e. V /\ ( E ` F ) = { x } ) -> E. y e. V ( E ` F ) = { x , y } )
28 16 23 27 syl2anc 
 |-  ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) = (/) ) -> E. y e. V ( E ` F ) = { x , y } )
29 n0 
 |-  ( ( ( E ` F ) \ { x } ) =/= (/) <-> E. y y e. ( ( E ` F ) \ { x } ) )
30 14 adantr 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( E ` F ) C_ V )
31 simprr 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> y e. ( ( E ` F ) \ { x } ) )
32 31 eldifad 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> y e. ( E ` F ) )
33 30 32 sseldd 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> y e. V )
34 1 2 upgrfi 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E ` F ) e. Fin )
35 34 adantr 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( E ` F ) e. Fin )
36 simprl 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> x e. ( E ` F ) )
37 36 32 prssd 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> { x , y } C_ ( E ` F ) )
38 fvex 
 |-  ( E ` F ) e. _V
39 ssdomg 
 |-  ( ( E ` F ) e. _V -> ( { x , y } C_ ( E ` F ) -> { x , y } ~<_ ( E ` F ) ) )
40 38 37 39 mpsyl 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> { x , y } ~<_ ( E ` F ) )
41 1 2 upgrle 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( # ` ( E ` F ) ) <_ 2 )
42 41 adantr 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( # ` ( E ` F ) ) <_ 2 )
43 eldifsni 
 |-  ( y e. ( ( E ` F ) \ { x } ) -> y =/= x )
44 43 ad2antll 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> y =/= x )
45 44 necomd 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> x =/= y )
46 hashprg 
 |-  ( ( x e. _V /\ y e. _V ) -> ( x =/= y <-> ( # ` { x , y } ) = 2 ) )
47 46 el2v 
 |-  ( x =/= y <-> ( # ` { x , y } ) = 2 )
48 45 47 sylib 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( # ` { x , y } ) = 2 )
49 42 48 breqtrrd 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( # ` ( E ` F ) ) <_ ( # ` { x , y } ) )
50 prfi 
 |-  { x , y } e. Fin
51 hashdom 
 |-  ( ( ( E ` F ) e. Fin /\ { x , y } e. Fin ) -> ( ( # ` ( E ` F ) ) <_ ( # ` { x , y } ) <-> ( E ` F ) ~<_ { x , y } ) )
52 35 50 51 sylancl 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( ( # ` ( E ` F ) ) <_ ( # ` { x , y } ) <-> ( E ` F ) ~<_ { x , y } ) )
53 49 52 mpbid 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( E ` F ) ~<_ { x , y } )
54 sbth 
 |-  ( ( { x , y } ~<_ ( E ` F ) /\ ( E ` F ) ~<_ { x , y } ) -> { x , y } ~~ ( E ` F ) )
55 40 53 54 syl2anc 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> { x , y } ~~ ( E ` F ) )
56 fisseneq 
 |-  ( ( ( E ` F ) e. Fin /\ { x , y } C_ ( E ` F ) /\ { x , y } ~~ ( E ` F ) ) -> { x , y } = ( E ` F ) )
57 35 37 55 56 syl3anc 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> { x , y } = ( E ` F ) )
58 57 eqcomd 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( E ` F ) = { x , y } )
59 33 58 jca 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ ( x e. ( E ` F ) /\ y e. ( ( E ` F ) \ { x } ) ) ) -> ( y e. V /\ ( E ` F ) = { x , y } ) )
60 59 expr 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> ( y e. ( ( E ` F ) \ { x } ) -> ( y e. V /\ ( E ` F ) = { x , y } ) ) )
61 60 eximdv 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> ( E. y y e. ( ( E ` F ) \ { x } ) -> E. y ( y e. V /\ ( E ` F ) = { x , y } ) ) )
62 61 imp 
 |-  ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ E. y y e. ( ( E ` F ) \ { x } ) ) -> E. y ( y e. V /\ ( E ` F ) = { x , y } ) )
63 df-rex 
 |-  ( E. y e. V ( E ` F ) = { x , y } <-> E. y ( y e. V /\ ( E ` F ) = { x , y } ) )
64 62 63 sylibr 
 |-  ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ E. y y e. ( ( E ` F ) \ { x } ) ) -> E. y e. V ( E ` F ) = { x , y } )
65 29 64 sylan2b 
 |-  ( ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) /\ ( ( E ` F ) \ { x } ) =/= (/) ) -> E. y e. V ( E ` F ) = { x , y } )
66 28 65 pm2.61dane 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> E. y e. V ( E ` F ) = { x , y } )
67 15 66 jca 
 |-  ( ( ( G e. UPGraph /\ E Fn A /\ F e. A ) /\ x e. ( E ` F ) ) -> ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) )
68 67 ex 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( x e. ( E ` F ) -> ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) ) )
69 68 eximdv 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> ( E. x x e. ( E ` F ) -> E. x ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) ) )
70 5 69 mpd 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> E. x ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) )
71 df-rex 
 |-  ( E. x e. V E. y e. V ( E ` F ) = { x , y } <-> E. x ( x e. V /\ E. y e. V ( E ` F ) = { x , y } ) )
72 70 71 sylibr 
 |-  ( ( G e. UPGraph /\ E Fn A /\ F e. A ) -> E. x e. V E. y e. V ( E ` F ) = { x , y } )