Metamath Proof Explorer


Theorem usgrislfuspgr

Description: A simple graph is a loop-free simple pseudograph. (Contributed by AV, 27-Jan-2021)

Ref Expression
Hypotheses usgrislfuspgr.v V = Vtx G
usgrislfuspgr.i I = iEdg G
Assertion usgrislfuspgr G USGraph G USHGraph I : dom I x 𝒫 V | 2 x

Proof

Step Hyp Ref Expression
1 usgrislfuspgr.v V = Vtx G
2 usgrislfuspgr.i I = iEdg G
3 usgruspgr G USGraph G USHGraph
4 1 2 usgrfs G USGraph I : dom I 1-1 x 𝒫 V | x = 2
5 f1f I : dom I 1-1 x 𝒫 V | x = 2 I : dom I x 𝒫 V | x = 2
6 2re 2
7 6 leidi 2 2
8 7 a1i x = 2 2 2
9 breq2 x = 2 2 x 2 2
10 8 9 mpbird x = 2 2 x
11 10 a1i x 𝒫 V x = 2 2 x
12 11 ss2rabi x 𝒫 V | x = 2 x 𝒫 V | 2 x
13 12 a1i I : dom I 1-1 x 𝒫 V | x = 2 x 𝒫 V | x = 2 x 𝒫 V | 2 x
14 5 13 fssd I : dom I 1-1 x 𝒫 V | x = 2 I : dom I x 𝒫 V | 2 x
15 4 14 syl G USGraph I : dom I x 𝒫 V | 2 x
16 3 15 jca G USGraph G USHGraph I : dom I x 𝒫 V | 2 x
17 1 2 uspgrf G USHGraph I : dom I 1-1 x 𝒫 V | x 2
18 df-f1 I : dom I 1-1 x 𝒫 V | x 2 I : dom I x 𝒫 V | x 2 Fun I -1
19 fin I : dom I x 𝒫 V | x 2 x 𝒫 V | 2 x I : dom I x 𝒫 V | x 2 I : dom I x 𝒫 V | 2 x
20 umgrislfupgrlem x 𝒫 V | x 2 x 𝒫 V | 2 x = x 𝒫 V | x = 2
21 feq3 x 𝒫 V | x 2 x 𝒫 V | 2 x = x 𝒫 V | x = 2 I : dom I x 𝒫 V | x 2 x 𝒫 V | 2 x I : dom I x 𝒫 V | x = 2
22 20 21 ax-mp I : dom I x 𝒫 V | x 2 x 𝒫 V | 2 x I : dom I x 𝒫 V | x = 2
23 19 22 sylbb1 I : dom I x 𝒫 V | x 2 I : dom I x 𝒫 V | 2 x I : dom I x 𝒫 V | x = 2
24 23 anim1i I : dom I x 𝒫 V | x 2 I : dom I x 𝒫 V | 2 x Fun I -1 I : dom I x 𝒫 V | x = 2 Fun I -1
25 df-f1 I : dom I 1-1 x 𝒫 V | x = 2 I : dom I x 𝒫 V | x = 2 Fun I -1
26 24 25 sylibr I : dom I x 𝒫 V | x 2 I : dom I x 𝒫 V | 2 x Fun I -1 I : dom I 1-1 x 𝒫 V | x = 2
27 26 ex I : dom I x 𝒫 V | x 2 I : dom I x 𝒫 V | 2 x Fun I -1 I : dom I 1-1 x 𝒫 V | x = 2
28 27 impancom I : dom I x 𝒫 V | x 2 Fun I -1 I : dom I x 𝒫 V | 2 x I : dom I 1-1 x 𝒫 V | x = 2
29 18 28 sylbi I : dom I 1-1 x 𝒫 V | x 2 I : dom I x 𝒫 V | 2 x I : dom I 1-1 x 𝒫 V | x = 2
30 29 imp I : dom I 1-1 x 𝒫 V | x 2 I : dom I x 𝒫 V | 2 x I : dom I 1-1 x 𝒫 V | x = 2
31 17 30 sylan G USHGraph I : dom I x 𝒫 V | 2 x I : dom I 1-1 x 𝒫 V | x = 2
32 1 2 isusgr G USHGraph G USGraph I : dom I 1-1 x 𝒫 V | x = 2
33 32 adantr G USHGraph I : dom I x 𝒫 V | 2 x G USGraph I : dom I 1-1 x 𝒫 V | x = 2
34 31 33 mpbird G USHGraph I : dom I x 𝒫 V | 2 x G USGraph
35 16 34 impbii G USGraph G USHGraph I : dom I x 𝒫 V | 2 x