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 ↾ P v n ⊆ 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 → v n ∈ 𝒫 V
5 2 3 4 syl2an ⊢ V ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → v n ∈ 𝒫 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 ↔ v n = 2
10 2 3 9 syl2an ⊢ V ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → v ≠ n ↔ v n = 2
11 8 10 mpbid ⊢ V ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → v n = 2
12 fveqeq2 ⊢ x = v n → x = 2 ↔ v n = 2
13 rnresi ⊢ ran ⁡ I ↾ P = P
14 13 1 eqtri ⊢ ran ⁡ I ↾ P = x ∈ 𝒫 V | x = 2
15 12 14 elrab2 ⊢ v n ∈ ran ⁡ I ↾ P ↔ v n ∈ 𝒫 V ∧ v n = 2
16 5 11 15 sylanbrc ⊢ V ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → v n ∈ ran ⁡ I ↾ P
17 sseq2 ⊢ e = v n → v n ⊆ e ↔ v n ⊆ v n
18 17 adantl ⊢ V ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v ∧ e = v n → v n ⊆ e ↔ v n ⊆ v n
19 ssidd ⊢ V ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → v n ⊆ v n
20 16 18 19 rspcedvd ⊢ V ∈ W ∧ v ∈ V ∧ n ∈ V ∖ v → ∃ e ∈ ran ⁡ I ↾ P v n ⊆ e