This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem umgrislfupgr

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

Ref Expression
Hypotheses umgrislfupgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
umgrislfupgr.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion umgrislfupgr ( 𝐺 ∈ UMGraph ↔ ( 𝐺 ∈ UPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )

Proof

Step Hyp Ref Expression
1 umgrislfupgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 umgrislfupgr.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 umgrupgr ⊢ ( 𝐺 ∈ UMGraph → 𝐺 ∈ UPGraph )
4 1 2 umgrf ⊢ ( 𝐺 ∈ UMGraph → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 id ⊢ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
6 2re ⊢ 2 ∈ ℝ
7 6 leidi ⊢ 2 ≤ 2
8 7 a1i ⊢ ( ( ♯ ‘ 𝑥 ) = 2 → 2 ≤ 2 )
9 breq2 ⊢ ( ( ♯ ‘ 𝑥 ) = 2 → ( 2 ≤ ( ♯ ‘ 𝑥 ) ↔ 2 ≤ 2 ) )
10 8 9 mpbird ⊢ ( ( ♯ ‘ 𝑥 ) = 2 → 2 ≤ ( ♯ ‘ 𝑥 ) )
11 10 a1i ⊢ ( 𝑥 ∈ 𝒫 𝑉 → ( ( ♯ ‘ 𝑥 ) = 2 → 2 ≤ ( ♯ ‘ 𝑥 ) ) )
12 11 ss2rabi ⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
13 12 a1i ⊢ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
14 5 13 fssd ⊢ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
15 4 14 syl ⊢ ( 𝐺 ∈ UMGraph → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
16 3 15 jca ⊢ ( 𝐺 ∈ UMGraph → ( 𝐺 ∈ UPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
17 1 2 upgrf ⊢ ( 𝐺 ∈ UPGraph → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
18 fin ⊢ ( 𝐼 : dom 𝐼 ⟶ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) ↔ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
19 umgrislfupgrlem ⊢ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
20 feq3 ⊢ ( ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( 𝐼 : dom 𝐼 ⟶ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) ↔ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
21 19 20 ax-mp ⊢ ( 𝐼 : dom 𝐼 ⟶ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) ↔ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
22 18 21 sylbb1 ⊢ ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
23 17 22 sylan ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
24 1 2 isumgr ⊢ ( 𝐺 ∈ UPGraph → ( 𝐺 ∈ UMGraph ↔ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
25 24 adantr ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → ( 𝐺 ∈ UMGraph ↔ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
26 23 25 mpbird ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐺 ∈ UMGraph )
27 16 26 impbii ⊢ ( 𝐺 ∈ UMGraph ↔ ( 𝐺 ∈ UPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )