# Metamath Proof Explorer

## Theorem cusgrexilem2

Description: Lemma 2 for cusgrexi . (Contributed by AV, 12-Jan-2018) (Revised by AV, 10-Nov-2021)

Ref Expression
Hypothesis usgrexi.p 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
Assertion cusgrexilem2 ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ∃ 𝑒 ∈ ran ( I ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 )

### Proof

Step Hyp Ref Expression
1 usgrexi.p 𝑃 = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
2 simpr ( ( 𝑉𝑊𝑣𝑉 ) → 𝑣𝑉 )
3 eldifi ( 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) → 𝑛𝑉 )
4 prelpwi ( ( 𝑣𝑉𝑛𝑉 ) → { 𝑣 , 𝑛 } ∈ 𝒫 𝑉 )
5 2 3 4 syl2an ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → { 𝑣 , 𝑛 } ∈ 𝒫 𝑉 )
6 eldifsni ( 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) → 𝑛𝑣 )
7 6 necomd ( 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) → 𝑣𝑛 )
8 7 adantl ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → 𝑣𝑛 )
9 hashprg ( ( 𝑣𝑉𝑛𝑉 ) → ( 𝑣𝑛 ↔ ( ♯ ‘ { 𝑣 , 𝑛 } ) = 2 ) )
10 2 3 9 syl2an ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( 𝑣𝑛 ↔ ( ♯ ‘ { 𝑣 , 𝑛 } ) = 2 ) )
11 8 10 mpbid ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ( ♯ ‘ { 𝑣 , 𝑛 } ) = 2 )
12 fveqeq2 ( 𝑥 = { 𝑣 , 𝑛 } → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ♯ ‘ { 𝑣 , 𝑛 } ) = 2 ) )
13 rnresi ran ( I ↾ 𝑃 ) = 𝑃
14 13 1 eqtri ran ( I ↾ 𝑃 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 2 }
15 12 14 elrab2 ( { 𝑣 , 𝑛 } ∈ ran ( I ↾ 𝑃 ) ↔ ( { 𝑣 , 𝑛 } ∈ 𝒫 𝑉 ∧ ( ♯ ‘ { 𝑣 , 𝑛 } ) = 2 ) )
16 5 11 15 sylanbrc ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → { 𝑣 , 𝑛 } ∈ ran ( I ↾ 𝑃 ) )
17 sseq2 ( 𝑒 = { 𝑣 , 𝑛 } → ( { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ { 𝑣 , 𝑛 } ⊆ { 𝑣 , 𝑛 } ) )
18 17 adantl ( ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) ∧ 𝑒 = { 𝑣 , 𝑛 } ) → ( { 𝑣 , 𝑛 } ⊆ 𝑒 ↔ { 𝑣 , 𝑛 } ⊆ { 𝑣 , 𝑛 } ) )
19 ssidd ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → { 𝑣 , 𝑛 } ⊆ { 𝑣 , 𝑛 } )
20 16 18 19 rspcedvd ( ( ( 𝑉𝑊𝑣𝑉 ) ∧ 𝑛 ∈ ( 𝑉 ∖ { 𝑣 } ) ) → ∃ 𝑒 ∈ ran ( I ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 )