Theorem isuslgra 23418

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 5704	. . . 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 466	. . 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 5143	. . . . 5 |- ( e = E -> dom e = dom E )
4	3	adantl 466	. . . 4 |- ( ( v = V /\ e = E ) -> dom e = dom E )
5		f1eq2 5705	. . . 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 16	. . 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 457	. . . . . 6 |- ( ( v = V /\ e = E ) -> v = V )
8	7	pweqd 3968	. . . . 5 |- ( ( v = V /\ e = E ) -> ~P v = ~P V )
9	8	difeq1d 3576	. . . 4 |- ( ( v = V /\ e = E ) -> ( ~P v \ { (/) } ) = ( ~P V \ { (/) } ) )
10		rabeq 3066	. . . 4 |- ( ( ~P v \ { (/) } ) = ( ~P V \ { (/) } ) -> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } = { x e. ( ~P V \ { (/) } ) | ( # ` x ) <_ 2 } )
11		f1eq3 5706	. . . 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 20	. . 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 279	. 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 23412	. 2 |- USLGrph = { <. v , e >. | e : dom e -1-1-> { x e. ( ~P v \ { (/) } ) | ( # ` x ) <_ 2 } }
15	13, 14	brabga 4706	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 184   /\ wa 369   = wceq 1370   e. wcel 1758   {crab 2800   \ cdif 3428   (/)c0 3740   ~Pcpw 3963   {csn 3980   class class class wbr 4395   dom cdm 4943   -1-1->wf1 5518   ` cfv 5521   <_ cle 9525   2c2 10477   #chash 12215   USLGrph cuslg 23410

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1954  ax-ext 2431  ax-sep 4516  ax-nul 4524  ax-pr 4634

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2265  df-mo 2266  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2602  df-ne 2647  df-rab 2805  df-v 3074  df-dif 3434  df-un 3436  df-in 3438  df-ss 3445  df-nul 3741  df-if 3895  df-pw 3965  df-sn 3981  df-pr 3983  df-op 3987  df-br 4396  df-opab 4454  df-rel 4950  df-cnv 4951  df-co 4952  df-dm 4953  df-rn 4954  df-fun 5523  df-fn 5524  df-f 5525  df-f1 5526  df-uslgra 23412

This theorem is referenced by:  uslgraf  23420  uslisumgra  23432  usisuslgra  23433  uslgra1  23438