Theorem umgrislfupgrlem

Description: Lemma for umgrislfupgr and usgrislfuspgr . (Contributed by AV, 27-Jan-2021)

	Ref	Expression
Assertion	umgrislfupgrlem	⊢ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }

Proof

Step	Hyp	Ref	Expression
1		2pos	⊢ 0 < 2
2		simprl	⊢ ( ( 0 < 2 ∧ ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝒫 𝑉 )
3		fveq2	⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ∅ ) )
4		hash0	⊢ ( ♯ ‘ ∅ ) = 0
5	3 4	eqtrdi	⊢ ( 𝑥 = ∅ → ( ♯ ‘ 𝑥 ) = 0 )
6	5	breq2d	⊢ ( 𝑥 = ∅ → ( 2 ≤ ( ♯ ‘ 𝑥 ) ↔ 2 ≤ 0 ) )
7		2re	⊢ 2 ∈ ℝ
8		0re	⊢ 0 ∈ ℝ
9	7 8	lenlti	⊢ ( 2 ≤ 0 ↔ ¬ 0 < 2 )
10		pm2.21	⊢ ( ¬ 0 < 2 → ( 0 < 2 → 𝑥 ≠ ∅ ) )
11	9 10	sylbi	⊢ ( 2 ≤ 0 → ( 0 < 2 → 𝑥 ≠ ∅ ) )
12	6 11	syl6bi	⊢ ( 𝑥 = ∅ → ( 2 ≤ ( ♯ ‘ 𝑥 ) → ( 0 < 2 → 𝑥 ≠ ∅ ) ) )
13	12	adantld	⊢ ( 𝑥 = ∅ → ( ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) → ( 0 < 2 → 𝑥 ≠ ∅ ) ) )
14	13	impcomd	⊢ ( 𝑥 = ∅ → ( ( 0 < 2 ∧ ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) → 𝑥 ≠ ∅ ) )
15		ax-1	⊢ ( 𝑥 ≠ ∅ → ( ( 0 < 2 ∧ ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) → 𝑥 ≠ ∅ ) )
16	14 15	pm2.61ine	⊢ ( ( 0 < 2 ∧ ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) → 𝑥 ≠ ∅ )
17		eldifsn	⊢ ( 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ↔ ( 𝑥 ∈ 𝒫 𝑉 ∧ 𝑥 ≠ ∅ ) )
18	2 16 17	sylanbrc	⊢ ( ( 0 < 2 ∧ ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) → 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) )
19		simprr	⊢ ( ( 0 < 2 ∧ ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) → 2 ≤ ( ♯ ‘ 𝑥 ) )
20	18 19	jca	⊢ ( ( 0 < 2 ∧ ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) )
21	20	ex	⊢ ( 0 < 2 → ( ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) → ( 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) )
22		eldifi	⊢ ( 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) → 𝑥 ∈ 𝒫 𝑉 )
23	22	anim1i	⊢ ( ( 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) )
24	21 23	impbid1	⊢ ( 0 < 2 → ( ( 𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) )
25	24	rabbidva2	⊢ ( 0 < 2 → { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
26	1 25	ax-mp	⊢ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) }
27	26	ineq2i	⊢ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) = ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } )
28		inrab	⊢ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ( ♯ ‘ 𝑥 ) ≤ 2 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) }
29		hashxnn0	⊢ ( 𝑥 ∈ V → ( ♯ ‘ 𝑥 ) ∈ ℕ0* )
30	29	elv	⊢ ( ♯ ‘ 𝑥 ) ∈ ℕ0*
31		xnn0xr	⊢ ( ( ♯ ‘ 𝑥 ) ∈ ℕ0* → ( ♯ ‘ 𝑥 ) ∈ ℝ* )
32	30 31	ax-mp	⊢ ( ♯ ‘ 𝑥 ) ∈ ℝ*
33	7	rexri	⊢ 2 ∈ ℝ*
34		xrletri3	⊢ ( ( ( ♯ ‘ 𝑥 ) ∈ ℝ* ∧ 2 ∈ ℝ* ) → ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ( ♯ ‘ 𝑥 ) ≤ 2 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ) )
35	32 33 34	mp2an	⊢ ( ( ♯ ‘ 𝑥 ) = 2 ↔ ( ( ♯ ‘ 𝑥 ) ≤ 2 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) )
36	35	bicomi	⊢ ( ( ( ♯ ‘ 𝑥 ) ≤ 2 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) ↔ ( ♯ ‘ 𝑥 ) = 2 )
37	36	rabbii	⊢ { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ( ♯ ‘ 𝑥 ) ≤ 2 ∧ 2 ≤ ( ♯ ‘ 𝑥 ) ) } = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }
38	27 28 37	3eqtri	⊢ ( { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) ≤ 2 } ∩ { 𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ ( ♯ ‘ 𝑥 ) } ) = { 𝑥 ∈ ( 𝒫 𝑉 ∖ { ∅ } ) ∣ ( ♯ ‘ 𝑥 ) = 2 }