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

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 ↾ 𝑃 ) { 𝑣 , 𝑛 } ⊆ 𝑒 )