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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
usgrislfuspgr.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
Assertion usgrislfuspgr ( 𝐺 ∈ USGraph ↔ ( 𝐺 ∈ USPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )

Proof

Step Hyp Ref Expression
1 usgrislfuspgr.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 usgrislfuspgr.i ⊢ 𝐼 = ( iEdg ‘ 𝐺 )
3 usgruspgr ⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
4 1 2 usgrfs ⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 f1f ⊢ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 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 𝐼 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
14 5 13 fssd ⊢ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
15 4 14 syl ⊢ ( 𝐺 ∈ USGraph → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
16 3 15 jca ⊢ ( 𝐺 ∈ USGraph → ( 𝐺 ∈ USPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
17 1 2 uspgrf ⊢ ( 𝐺 ∈ USPGraph → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
18 df-f1 ⊢ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ↔ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ Fun ◡ 𝐼 ) )
19 fin ⊢ ( 𝐼 : dom 𝐼 ⟶ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) ↔ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )
20 umgrislfupgrlem ⊢ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
21 feq3 ⊢ ( ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( 𝐼 : dom 𝐼 ⟶ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) ↔ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
22 20 21 ax-mp ⊢ ( 𝐼 : dom 𝐼 ⟶ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) ↔ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
23 19 22 sylbb1 ⊢ ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
24 23 anim1i ⊢ ( ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) ∧ Fun ◡ 𝐼 ) → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ Fun ◡ 𝐼 ) )
25 df-f1 ⊢ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ↔ ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ∧ Fun ◡ 𝐼 ) )
26 24 25 sylibr ⊢ ( ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) ∧ Fun ◡ 𝐼 ) → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
27 26 ex ⊢ ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → ( Fun ◡ 𝐼 → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
28 27 impancom ⊢ ( ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ Fun ◡ 𝐼 ) → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
29 18 28 sylbi ⊢ ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } → ( 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
30 29 imp ⊢ ( ( 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
31 17 30 sylan ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } )
32 1 2 isusgr ⊢ ( 𝐺 ∈ USPGraph → ( 𝐺 ∈ USGraph ↔ 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
33 32 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → ( 𝐺 ∈ USGraph ↔ 𝐼 : dom 𝐼 –1-1→ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
34 31 33 mpbird ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) → 𝐺 ∈ USGraph )
35 16 34 impbii ⊢ ( 𝐺 ∈ USGraph ↔ ( 𝐺 ∈ USPGraph ∧ 𝐼 : dom 𝐼 ⟶ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) )