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

Metamath Proof Explorer

Theorem upgr1elem

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

Ref Expression
Hypotheses upgr1elem.s ⊢ ( 𝜑 → { 𝐵 , 𝐶 } ∈ 𝑆 )
upgr1elem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
Assertion upgr1elem ( 𝜑 → { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( 𝑆 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )

Proof

Step Hyp Ref Expression
1 upgr1elem.s ⊢ ( 𝜑 → { 𝐵 , 𝐶 } ∈ 𝑆 )
2 upgr1elem.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
3 fveq2 ⊢ ( 𝑥 = { 𝐵 , 𝐶 } → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ { 𝐵 , 𝐶 } ) )
4 3 breq1d ⊢ ( 𝑥 = { 𝐵 , 𝐶 } → ( ( ♯ ‘ 𝑥 ) ≤ 2 ↔ ( ♯ ‘ { 𝐵 , 𝐶 } ) ≤ 2 ) )
5 prnzg ⊢ ( 𝐵 ∈ 𝑊 → { 𝐵 , 𝐶 } ≠ ∅ )
6 2 5 syl ⊢ ( 𝜑 → { 𝐵 , 𝐶 } ≠ ∅ )
7 eldifsn ⊢ ( { 𝐵 , 𝐶 } ∈ ( 𝑆 ∖ { ∅ } ) ↔ ( { 𝐵 , 𝐶 } ∈ 𝑆 ∧ { 𝐵 , 𝐶 } ≠ ∅ ) )
8 1 6 7 sylanbrc ⊢ ( 𝜑 → { 𝐵 , 𝐶 } ∈ ( 𝑆 ∖ { ∅ } ) )
9 hashprlei ⊢ ( { 𝐵 , 𝐶 } ∈ Fin ∧ ( ♯ ‘ { 𝐵 , 𝐶 } ) ≤ 2 )
10 9 simpri ⊢ ( ♯ ‘ { 𝐵 , 𝐶 } ) ≤ 2
11 10 a1i ⊢ ( 𝜑 → ( ♯ ‘ { 𝐵 , 𝐶 } ) ≤ 2 )
12 4 8 11 elrabd ⊢ ( 𝜑 → { 𝐵 , 𝐶 } ∈ { 𝑥 ∈ ( 𝑆 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )
13 12 snssd ⊢ ( 𝜑 → { { 𝐵 , 𝐶 } } ⊆ { 𝑥 ∈ ( 𝑆 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } )