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

Metamath Proof Explorer

Theorem cusgrfilem1

Description: Lemma 1 for cusgrfi . (Contributed by Alexander van der Vekens, 13-Jan-2018) (Revised by AV, 11-Nov-2020)

Ref Expression
Hypotheses cusgrfi.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
cusgrfi.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) }
Assertion cusgrfilem1 ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑃 ⊆ ( Edg ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 cusgrfi.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 cusgrfi.p ⊢ 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) }
3 eqid ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
4 1 3 cusgredg ⊢ ( 𝐺 ∈ ComplUSGraph → ( Edg ‘ 𝐺 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
5 fveq2 ⊢ ( 𝑥 = { 𝑎 , 𝑁 } → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝑎 , 𝑁 } ) )
6 5 ad2antlr ⊢ ( ( ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑉 ) ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝑎 , 𝑁 } ) )
7 hashprg ⊢ ( ( 𝑎 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) → ( 𝑎 ≠ 𝑁 ↔ ( ♯ ‘ { 𝑎 , 𝑁 } ) = 2 ) )
8 7 adantrr ⊢ ( ( 𝑎 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑉 ) ) → ( 𝑎 ≠ 𝑁 ↔ ( ♯ ‘ { 𝑎 , 𝑁 } ) = 2 ) )
9 8 biimpcd ⊢ ( 𝑎 ≠ 𝑁 → ( ( 𝑎 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑉 ) ) → ( ♯ ‘ { 𝑎 , 𝑁 } ) = 2 ) )
10 9 adantr ⊢ ( ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) → ( ( 𝑎 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑉 ) ) → ( ♯ ‘ { 𝑎 , 𝑁 } ) = 2 ) )
11 10 imp ⊢ ( ( ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑉 ) ) ) → ( ♯ ‘ { 𝑎 , 𝑁 } ) = 2 )
12 6 11 eqtrd ⊢ ( ( ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑉 ) ) ) → ( ♯ ‘ 𝑥 ) = 2 )
13 12 an13s ⊢ ( ( ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑉 ) ∧ ( 𝑎 ∈ 𝑉 ∧ ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) ) ) → ( ♯ ‘ 𝑥 ) = 2 )
14 13 rexlimdvaa ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝑥 ∈ 𝒫 𝑉 ) → ( ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) → ( ♯ ‘ 𝑥 ) = 2 ) )
15 14 ss2rabdv ⊢ ( 𝑁 ∈ 𝑉 → { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) } ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
16 2 a1i ⊢ ( ( Edg ‘ 𝐺 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) } )
17 id ⊢ ( ( Edg ‘ 𝐺 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( Edg ‘ 𝐺 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } )
18 16 17 sseq12d ⊢ ( ( Edg ‘ 𝐺 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( 𝑃 ⊆ ( Edg ‘ 𝐺 ) ↔ { 𝑥 ∈ 𝒫 𝑉 ∣ ∃ 𝑎 ∈ 𝑉 ( 𝑎 ≠ 𝑁 ∧ 𝑥 = { 𝑎 , 𝑁 } ) } ⊆ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } ) )
19 15 18 imbitrrid ⊢ ( ( Edg ‘ 𝐺 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( 𝑁 ∈ 𝑉 → 𝑃 ⊆ ( Edg ‘ 𝐺 ) ) )
20 4 19 syl ⊢ ( 𝐺 ∈ ComplUSGraph → ( 𝑁 ∈ 𝑉 → 𝑃 ⊆ ( Edg ‘ 𝐺 ) ) )
21 20 imp ⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑃 ⊆ ( Edg ‘ 𝐺 ) )