Theorem isuslgra 25082

Description: The property of being an undirected simple graph with loops. (Contributed by Alexander van der Vekens, 10-Aug-2017.)

Assertion

Ref	Expression
isuslgra	|- ( ( V e. W /\ E e. X ) -> ( V USLGrph E <-> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )

Distinct variable groups:   x, E   x, V

Allowed substitution hints:   W( x)   X( x)

Proof of Theorem isuslgra

Dummy variables v e are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1eq1 5757	. . . 4 |- ( e = E -> ( e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> E : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } ) )
2	1	adantl 472	. . 3 |- ( ( v = V /\ e = E ) -> ( e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> E : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } ) )
3		dmeq 5013	. . . . 5 |- ( e = E -> dom e = dom E )
4	3	adantl 472	. . . 4 |- ( ( v = V /\ e = E ) -> dom e = dom E )
5		f1eq2 5758	. . . 4 |- ( dom e = dom E -> ( E : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> E : dom E -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } ) )
6	4, 5	syl 17	. . 3 |- ( ( v = V /\ e = E ) -> ( E : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> E : dom E -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } ) )
7		simpl 463	. . . . . 6 |- ( ( v = V /\ e = E ) -> v = V )
8	7	pweqd 3924	. . . . 5 |- ( ( v = V /\ e = E ) -> ~P v = ~P V )
9	8	difeq1d 3518	. . . 4 |- ( ( v = V /\ e = E ) -> ( ~P v \ { (/) } ) = ( ~P V \ { (/) } ) )
10		rabeq 3006	. . . 4 |- ( ( ~P v \ { (/) } ) = ( ~P V \ { (/) } ) -> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } = { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
11		f1eq3 5759	. . . 4 |- ( { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } = { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } -> ( E : dom E -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
12	9, 10, 11	3syl 18	. . 3 |- ( ( v = V /\ e = E ) -> ( E : dom E -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
13	2, 6, 12	3bitrd 287	. 2 |- ( ( v = V /\ e = E ) -> ( e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } <-> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )
14		df-uslgra 25071	. 2 |- USLGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }
15	13, 14	brabga 4688	1 |- ( ( V e. W /\ E e. X ) -> ( V USLGrph E <-> E : dom E -1-1-> { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } ) )

Syntax hints:   -> wi 4   <-> wb 189   /\ wa 375   = wceq 1448   e. wcel 1891   {crab 2741   \ cdif 3369   (/)c0 3699   ~Pcpw 3919   {csn 3936   class class class wbr 4374   dom cdm 4812   -1-1->wf1 5558   ` cfv 5561   <_ cle 9663   2c2 10648   #chash 12509   USLGrph cuslg 25068

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pr 4612

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-rab 2746  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-op 3943  df-br 4375  df-opab 4434  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-uslgra 25071

This theorem is referenced by:  uslgraf  25084  uslisushgra  25102  uslisumgra  25103  usisuslgra  25104  uslgra1  25111