Theorem uhgrvd0nedgb 39595

Description: A vertex in a hypergraph has degree 0 iff there is no edge incident with the vertex. (Contributed by AV, 24-Dec-2020.)

Hypotheses

Ref	Expression
vtxdushgrfvedg.v	|- V = (Vtx ` G )
vtxdushgrfvedg.e	|- E = (Edg ` G )
vtxdushgrfvedg.d	|- D = (VtxDeg ` G )

Assertion

Ref	Expression
uhgrvd0nedgb	|- ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. i e. dom (iEdg ` G ) U e. ( (iEdg ` G ) ` i ) ) )

Distinct variable groups:   i, E   i, G   U, i   i, V

Allowed substitution hint:   D( i)

Proof of Theorem uhgrvd0nedgb

Step	Hyp	Ref	Expression
1		vtxdushgrfvedg.d	. . . . 5 |- D = (VtxDeg ` G )
2	1	fveq1i 5889	. . . 4 |- ( D ` U ) = ( (VtxDeg ` G ) ` U )
3		vtxdushgrfvedg.v	. . . . 5 |- V = (Vtx ` G )
4		eqid 2462	. . . . 5 |- (iEdg ` G ) = (iEdg ` G )
5		eqid 2462	. . . . 5 |- dom (iEdg ` G ) = dom (iEdg ` G )
6	3, 4, 5	vtxdgval 39579	. . . 4 |- ( ( G e. UHGraph /\ U e. V ) -> ( (VtxDeg ` G ) ` U ) = ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) ) )
7	2, 6	syl5eq 2508	. . 3 |- ( ( G e. UHGraph /\ U e. V ) -> ( D ` U ) = ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) ) )
8	7	eqeq1d 2464	. 2 |- ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) ) = 0 ) )
9		fvex 5898	. . . . . . 7 |- (iEdg ` G ) e. _V
10	9	dmex 6753	. . . . . 6 |- dom (iEdg ` G ) e. _V
11	10	rabex 4568	. . . . 5 |- { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } e. _V
12		hashxnn0 39136	. . . . 5 |- ( { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } e. _V -> ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) e. NN0* )
13	11, 12	ax-mp 5	. . . 4 |- ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) e. NN0*
14	10	rabex 4568	. . . . 5 |- { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } e. _V
15		hashxnn0 39136	. . . . 5 |- ( { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } e. _V -> ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) e. NN0* )
16	14, 15	ax-mp 5	. . . 4 |- ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) e. NN0*
17	13, 16	pm3.2i 461	. . 3 |- ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) e. NN0* /\ ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) e. NN0* )
18		xnn0xadd0 39134	. . 3 |- ( ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) e. NN0* /\ ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) e. NN0* ) -> ( ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) ) = 0 <-> ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) = 0 /\ ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) = 0 ) ) )
19	17, 18	mp1i 13	. 2 |- ( ( G e. UHGraph /\ U e. V ) -> ( ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) +e ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) ) = 0 <-> ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) = 0 /\ ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) = 0 ) ) )
20		hasheq0 12576	. . . . . 6 |- ( { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } e. _V -> ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) = 0 <-> { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } = (/) ) )
21	11, 20	ax-mp 5	. . . . 5 |- ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) = 0 <-> { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } = (/) )
22		hasheq0 12576	. . . . . 6 |- ( { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } e. _V -> ( ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) = 0 <-> { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } = (/) ) )
23	14, 22	ax-mp 5	. . . . 5 |- ( ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) = 0 <-> { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } = (/) )
24	21, 23	anbi12i 708	. . . 4 |- ( ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) = 0 /\ ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) = 0 ) <-> ( { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } = (/) /\ { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } = (/) ) )
25		rabeq0 3766	. . . . 5 |- ( { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } = (/) <-> A. i e. dom (iEdg ` G ) -. U e. ( (iEdg ` G ) ` i ) )
26		rabeq0 3766	. . . . 5 |- ( { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } = (/) <-> A. i e. dom (iEdg ` G ) -. ( (iEdg ` G ) ` i ) = { U } )
27	25, 26	anbi12i 708	. . . 4 |- ( ( { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } = (/) /\ { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } = (/) ) <-> ( A. i e. dom (iEdg ` G ) -. U e. ( (iEdg ` G ) ` i ) /\ A. i e. dom (iEdg ` G ) -. ( (iEdg ` G ) ` i ) = { U } ) )
28		ralnex 2846	. . . . . . 7 |- ( A. i e. dom (iEdg ` G ) -. ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) <-> -. E. i e. dom (iEdg ` G ) ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) )
29	28	bicomi 207	. . . . . 6 |- ( -. E. i e. dom (iEdg ` G ) ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) <-> A. i e. dom (iEdg ` G ) -. ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) )
30		ioran 497	. . . . . . 7 |- ( -. ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) <-> ( -. U e. ( (iEdg ` G ) ` i ) /\ -. ( (iEdg ` G ) ` i ) = { U } ) )
31	30	ralbii 2831	. . . . . 6 |- ( A. i e. dom (iEdg ` G ) -. ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) <-> A. i e. dom (iEdg ` G ) ( -. U e. ( (iEdg ` G ) ` i ) /\ -. ( (iEdg ` G ) ` i ) = { U } ) )
32		r19.26 2929	. . . . . 6 |- ( A. i e. dom (iEdg ` G ) ( -. U e. ( (iEdg ` G ) ` i ) /\ -. ( (iEdg ` G ) ` i ) = { U } ) <-> ( A. i e. dom (iEdg ` G ) -. U e. ( (iEdg ` G ) ` i ) /\ A. i e. dom (iEdg ` G ) -. ( (iEdg ` G ) ` i ) = { U } ) )
33	29, 31, 32	3bitri 279	. . . . 5 |- ( -. E. i e. dom (iEdg ` G ) ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) <-> ( A. i e. dom (iEdg ` G ) -. U e. ( (iEdg ` G ) ` i ) /\ A. i e. dom (iEdg ` G ) -. ( (iEdg ` G ) ` i ) = { U } ) )
34	33	bicomi 207	. . . 4 |- ( ( A. i e. dom (iEdg ` G ) -. U e. ( (iEdg ` G ) ` i ) /\ A. i e. dom (iEdg ` G ) -. ( (iEdg ` G ) ` i ) = { U } ) <-> -. E. i e. dom (iEdg ` G ) ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) )
35	24, 27, 34	3bitri 279	. . 3 |- ( ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) = 0 /\ ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) = 0 ) <-> -. E. i e. dom (iEdg ` G ) ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) )
36		snidg 4006	. . . . . . . . 9 |- ( U e. V -> U e. { U } )
37		eleq2 2529	. . . . . . . . 9 |- ( ( (iEdg ` G ) ` i ) = { U } -> ( U e. ( (iEdg ` G ) ` i ) <-> U e. { U } ) )
38	36, 37	syl5ibrcom 230	. . . . . . . 8 |- ( U e. V -> ( ( (iEdg ` G ) ` i ) = { U } -> U e. ( (iEdg ` G ) ` i ) ) )
39	38	adantl 472	. . . . . . 7 |- ( ( G e. UHGraph /\ U e. V ) -> ( ( (iEdg ` G ) ` i ) = { U } -> U e. ( (iEdg ` G ) ` i ) ) )
40		pm4.72 892	. . . . . . 7 |- ( ( ( (iEdg ` G ) ` i ) = { U } -> U e. ( (iEdg ` G ) ` i ) ) <-> ( U e. ( (iEdg ` G ) ` i ) <-> ( ( (iEdg ` G ) ` i ) = { U } \/ U e. ( (iEdg ` G ) ` i ) ) ) )
41	39, 40	sylib 201	. . . . . 6 |- ( ( G e. UHGraph /\ U e. V ) -> ( U e. ( (iEdg ` G ) ` i ) <-> ( ( (iEdg ` G ) ` i ) = { U } \/ U e. ( (iEdg ` G ) ` i ) ) ) )
42		orcom 393	. . . . . 6 |- ( ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) <-> ( ( (iEdg ` G ) ` i ) = { U } \/ U e. ( (iEdg ` G ) ` i ) ) )
43	41, 42	syl6rbbr 272	. . . . 5 |- ( ( G e. UHGraph /\ U e. V ) -> ( ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) <-> U e. ( (iEdg ` G ) ` i ) ) )
44	43	rexbidv 2913	. . . 4 |- ( ( G e. UHGraph /\ U e. V ) -> ( E. i e. dom (iEdg ` G ) ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) <-> E. i e. dom (iEdg ` G ) U e. ( (iEdg ` G ) ` i ) ) )
45	44	notbid 300	. . 3 |- ( ( G e. UHGraph /\ U e. V ) -> ( -. E. i e. dom (iEdg ` G ) ( U e. ( (iEdg ` G ) ` i ) \/ ( (iEdg ` G ) ` i ) = { U } ) <-> -. E. i e. dom (iEdg ` G ) U e. ( (iEdg ` G ) ` i ) ) )
46	35, 45	syl5bb 265	. 2 |- ( ( G e. UHGraph /\ U e. V ) -> ( ( ( # ` { i e. dom (iEdg ` G ) | U e. ( (iEdg ` G ) ` i ) } ) = 0 /\ ( # ` { i e. dom (iEdg ` G ) | ( (iEdg ` G ) ` i ) = { U } } ) = 0 ) <-> -. E. i e. dom (iEdg ` G ) U e. ( (iEdg ` G ) ` i ) ) )
47	8, 19, 46	3bitrd 287	1 |- ( ( G e. UHGraph /\ U e. V ) -> ( ( D ` U ) = 0 <-> -. E. i e. dom (iEdg ` G ) U e. ( (iEdg ` G ) ` i ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 189   \/ wo 374   /\ wa 375   = wceq 1455   e. wcel 1898   A.wral 2749   E.wrex 2750   {crab 2753   _Vcvv 3057   (/)c0 3743   {csn 3980   dom cdm 4853   ` cfv 5601  (class class class)co 6315   0cc0 9565   +ecxad 11436   #chash 12547  NN0*cxnn0 39116  Vtxcvtx 39147  iEdgciedg 39148   UHGraph cuhgr 39193  Edgcedga 39258  VtxDegcvtxdg 39576

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-er 7389  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-card 8399  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-n0 10899  df-z 10967  df-uz 11189  df-xadd 11439  df-fz 11814  df-hash 12548  df-xnn0 39117  df-vtxdg 39577

This theorem is referenced by:  vtxduhgr0nedg  39596  vtxduhgr0edgnel  39598