Metamath Proof Explorer

Theorem umgrislfupgr

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

Ref Expression
Hypotheses umgrislfupgr.v ⊢ V = Vtx ⁡ G
umgrislfupgr.i ⊢ I = iEdg ⁡ G
Assertion umgrislfupgr ⊢ G ∈ UMGraph ↔ G ∈ UPGraph ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x

Proof

Step Hyp Ref Expression
1 umgrislfupgr.v ⊢ V = Vtx ⁡ G
2 umgrislfupgr.i ⊢ I = iEdg ⁡ G
3 umgrupgr ⊢ G ∈ UMGraph → G ∈ UPGraph
4 1 2 umgrf ⊢ G ∈ UMGraph → I : dom ⁡ I ⟶ x ∈ 𝒫 V | x = 2
5 id ⊢ I : dom ⁡ I ⟶ 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 ⟶ x ∈ 𝒫 V | x = 2 → x ∈ 𝒫 V | x = 2 ⊆ x ∈ 𝒫 V | 2 ≤ x
14 5 13 fssd ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V | x = 2 → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x
15 4 14 syl ⊢ G ∈ UMGraph → I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x
16 3 15 jca ⊢ G ∈ UMGraph → G ∈ UPGraph ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x
17 1 2 upgrf ⊢ G ∈ UPGraph → I : dom ⁡ I ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2
18 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
19 umgrislfupgrlem ⊢ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 ∩ x ∈ 𝒫 V | 2 ≤ x = x ∈ 𝒫 V ∖ ∅ | x = 2
20 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
21 19 20 ax-mp ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 ∩ x ∈ 𝒫 V | 2 ≤ x ↔ I : dom ⁡ I ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2
22 18 21 sylbb1 ⊢ I : dom ⁡ I ⟶ x ∈ 𝒫 V ∖ ∅ | x ≤ 2 ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → I : dom ⁡ I ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2
23 17 22 sylan ⊢ G ∈ UPGraph ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → I : dom ⁡ I ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2
24 1 2 isumgr ⊢ G ∈ UPGraph → G ∈ UMGraph ↔ I : dom ⁡ I ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2
25 24 adantr ⊢ G ∈ UPGraph ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → G ∈ UMGraph ↔ I : dom ⁡ I ⟶ x ∈ 𝒫 V ∖ ∅ | x = 2
26 23 25 mpbird ⊢ G ∈ UPGraph ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x → G ∈ UMGraph
27 16 26 impbii ⊢ G ∈ UMGraph ↔ G ∈ UPGraph ∧ I : dom ⁡ I ⟶ x ∈ 𝒫 V | 2 ≤ x