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

Metamath Proof Explorer

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 biimtrdi ⊢ ( 𝑥 = ∅ → ( 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 }