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