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	syl5ibr	⊢ ( ( Edg ‘ 𝐺 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 } → ( 𝑁 ∈ 𝑉 → 𝑃 ⊆ ( Edg ‘ 𝐺 ) ) )
20	4 19	syl	⊢ ( 𝐺 ∈ ComplUSGraph → ( 𝑁 ∈ 𝑉 → 𝑃 ⊆ ( Edg ‘ 𝐺 ) ) )
21	20	imp	⊢ ( ( 𝐺 ∈ ComplUSGraph ∧ 𝑁 ∈ 𝑉 ) → 𝑃 ⊆ ( Edg ‘ 𝐺 ) )