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-1x∈𝒫V|x=2
5 f1f ⊢I:dom⁡I⟶1-1x∈𝒫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-1x∈𝒫V|x=2→x∈𝒫V|x=2⊆x∈𝒫V|2≤x
14 5 13 fssd ⊢I:dom⁡I⟶1-1x∈𝒫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-1x∈𝒫V∖∅|x≤2
18 df-f1 ⊢I:dom⁡I⟶1-1x∈𝒫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-1x∈𝒫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-1x∈𝒫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-1x∈𝒫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-1x∈𝒫V∖∅|x=2
29 18 28 sylbi ⊢I:dom⁡I⟶1-1x∈𝒫V∖∅|x≤2→I:dom⁡I⟶x∈𝒫V|2≤x→I:dom⁡I⟶1-1x∈𝒫V∖∅|x=2
30 29 imp ⊢I:dom⁡I⟶1-1x∈𝒫V∖∅|x≤2∧I:dom⁡I⟶x∈𝒫V|2≤x→I:dom⁡I⟶1-1x∈𝒫V∖∅|x=2
31 17 30 sylan ⊢G∈USHGraph∧I:dom⁡I⟶x∈𝒫V|2≤x→I:dom⁡I⟶1-1x∈𝒫V∖∅|x=2
32 1 2 isusgr ⊢G∈USHGraph→G∈USGraph↔I:dom⁡I⟶1-1x∈𝒫V∖∅|x=2
33 32 adantr ⊢G∈USHGraph∧I:dom⁡I⟶x∈𝒫V|2≤x→G∈USGraph↔I:dom⁡I⟶1-1x∈𝒫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