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 } )