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 ⊢P=x∈𝒫V|x=2
Assertion cusgrexilem2 ⊢V∈W∧v∈V∧n∈V∖v→∃e∈ran⁡I↾Pvn⊆e

Proof

Step Hyp Ref Expression
1 usgrexi.p ⊢P=x∈𝒫V|x=2
2 simpr ⊢V∈W∧v∈V→v∈V
3 eldifi ⊢n∈V∖v→n∈V
4 prelpwi ⊢v∈V∧n∈V→vn∈𝒫V
5 2 3 4 syl2an ⊢V∈W∧v∈V∧n∈V∖v→vn∈𝒫V
6 eldifsni ⊢n∈V∖v→n≠v
7 6 necomd ⊢n∈V∖v→v≠n
8 7 adantl ⊢V∈W∧v∈V∧n∈V∖v→v≠n
9 hashprg ⊢v∈V∧n∈V→v≠n↔vn=2
10 2 3 9 syl2an ⊢V∈W∧v∈V∧n∈V∖v→v≠n↔vn=2
11 8 10 mpbid ⊢V∈W∧v∈V∧n∈V∖v→vn=2
12 fveqeq2 ⊢x=vn→x=2↔vn=2
13 rnresi ⊢ran⁡I↾P=P
14 13 1 eqtri ⊢ran⁡I↾P=x∈𝒫V|x=2
15 12 14 elrab2 ⊢vn∈ran⁡I↾P↔vn∈𝒫V∧vn=2
16 5 11 15 sylanbrc ⊢V∈W∧v∈V∧n∈V∖v→vn∈ran⁡I↾P
17 sseq2 ⊢e=vn→vn⊆e↔vn⊆vn
18 17 adantl ⊢V∈W∧v∈V∧n∈V∖v∧e=vn→vn⊆e↔vn⊆vn
19 ssidd ⊢V∈W∧v∈V∧n∈V∖v→vn⊆vn
20 16 18 19 rspcedvd ⊢V∈W∧v∈V∧n∈V∖v→∃e∈ran⁡I↾Pvn⊆e