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