Metamath Proof Explorer

Theorem upgr1elem

Description: Lemma for upgr1e and uspgr1e . (Contributed by AV, 16-Oct-2020)

Ref Expression
Hypotheses upgr1elem.s ⊢ φ → B C ∈ S
upgr1elem.b ⊢ φ → B ∈ W
Assertion upgr1elem ⊢ φ → B C ⊆ x ∈ S ∖ ∅ | x ≤ 2

Proof

Step Hyp Ref Expression
1 upgr1elem.s ⊢ φ → B C ∈ S
2 upgr1elem.b ⊢ φ → B ∈ W
3 fveq2 ⊢ x = B C → x = B C
4 3 breq1d ⊢ x = B C → x ≤ 2 ↔ B C ≤ 2
5 prnzg ⊢ B ∈ W → B C ≠ ∅
6 2 5 syl ⊢ φ → B C ≠ ∅
7 eldifsn ⊢ B C ∈ S ∖ ∅ ↔ B C ∈ S ∧ B C ≠ ∅
8 1 6 7 sylanbrc ⊢ φ → B C ∈ S ∖ ∅
9 hashprlei ⊢ B C ∈ Fin ∧ B C ≤ 2
10 9 simpri ⊢ B C ≤ 2
11 10 a1i ⊢ φ → B C ≤ 2
12 4 8 11 elrabd ⊢ φ → B C ∈ x ∈ S ∖ ∅ | x ≤ 2
13 12 snssd ⊢ φ → B C ⊆ x ∈ S ∖ ∅ | x ≤ 2