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 ≤ ( ♯ ‘ 𝑥 ) } ) )