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 ⊢ V = Vtx ⁡ G
cusgrfi.p ⊢ P = x ∈ 𝒫 V | ∃ a ∈ V a ≠ N ∧ x = a N
Assertion cusgrfilem1 ⊢ G ∈ ComplUSGraph ∧ N ∈ V → P ⊆ Edg ⁡ G

Proof

Step Hyp Ref Expression
1 cusgrfi.v ⊢ V = Vtx ⁡ G
2 cusgrfi.p ⊢ P = x ∈ 𝒫 V | ∃ a ∈ V a ≠ N ∧ x = a N
3 eqid ⊢ Edg ⁡ G = Edg ⁡ G
4 1 3 cusgredg ⊢ G ∈ ComplUSGraph → Edg ⁡ G = x ∈ 𝒫 V | x = 2
5 fveq2 ⊢ x = a N → x = a N
6 5 ad2antlr ⊢ a ≠ N ∧ x = a N ∧ a ∈ V ∧ N ∈ V ∧ x ∈ 𝒫 V → x = a N
7 hashprg ⊢ a ∈ V ∧ N ∈ V → a ≠ N ↔ a N = 2
8 7 adantrr ⊢ a ∈ V ∧ N ∈ V ∧ x ∈ 𝒫 V → a ≠ N ↔ a N = 2
9 8 biimpcd ⊢ a ≠ N → a ∈ V ∧ N ∈ V ∧ x ∈ 𝒫 V → a N = 2
10 9 adantr ⊢ a ≠ N ∧ x = a N → a ∈ V ∧ N ∈ V ∧ x ∈ 𝒫 V → a N = 2
11 10 imp ⊢ a ≠ N ∧ x = a N ∧ a ∈ V ∧ N ∈ V ∧ x ∈ 𝒫 V → a N = 2
12 6 11 eqtrd ⊢ a ≠ N ∧ x = a N ∧ a ∈ V ∧ N ∈ V ∧ x ∈ 𝒫 V → x = 2
13 12 an13s ⊢ N ∈ V ∧ x ∈ 𝒫 V ∧ a ∈ V ∧ a ≠ N ∧ x = a N → x = 2
14 13 rexlimdvaa ⊢ N ∈ V ∧ x ∈ 𝒫 V → ∃ a ∈ V a ≠ N ∧ x = a N → x = 2
15 14 ss2rabdv ⊢ N ∈ V → x ∈ 𝒫 V | ∃ a ∈ V a ≠ N ∧ x = a N ⊆ x ∈ 𝒫 V | x = 2
16 2 a1i ⊢ Edg ⁡ G = x ∈ 𝒫 V | x = 2 → P = x ∈ 𝒫 V | ∃ a ∈ V a ≠ N ∧ x = a N
17 id ⊢ Edg ⁡ G = x ∈ 𝒫 V | x = 2 → Edg ⁡ G = x ∈ 𝒫 V | x = 2
18 16 17 sseq12d ⊢ Edg ⁡ G = x ∈ 𝒫 V | x = 2 → P ⊆ Edg ⁡ G ↔ x ∈ 𝒫 V | ∃ a ∈ V a ≠ N ∧ x = a N ⊆ x ∈ 𝒫 V | x = 2
19 15 18 imbitrrid ⊢ Edg ⁡ G = x ∈ 𝒫 V | x = 2 → N ∈ V → P ⊆ Edg ⁡ G
20 4 19 syl ⊢ G ∈ ComplUSGraph → N ∈ V → P ⊆ Edg ⁡ G
21 20 imp ⊢ G ∈ ComplUSGraph ∧ N ∈ V → P ⊆ Edg ⁡ G