Proof of Theorem umgrislfupgrlem
| Step | Hyp | Ref
| Expression |
| 1 | | 2pos 12369 |
. . . 4
⊢ 0 <
2 |
| 2 | | simprl 771 |
. . . . . . . . 9
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(♯‘𝑥))) →
𝑥 ∈ 𝒫 𝑉) |
| 3 | | fveq2 6906 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
(♯‘∅)) |
| 4 | | hash0 14406 |
. . . . . . . . . . . . . . 15
⊢
(♯‘∅) = 0 |
| 5 | 3, 4 | eqtrdi 2793 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ →
(♯‘𝑥) =
0) |
| 6 | 5 | breq2d 5155 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (2 ≤
(♯‘𝑥) ↔ 2
≤ 0)) |
| 7 | | 2re 12340 |
. . . . . . . . . . . . . . 15
⊢ 2 ∈
ℝ |
| 8 | | 0re 11263 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
| 9 | 7, 8 | lenlti 11381 |
. . . . . . . . . . . . . 14
⊢ (2 ≤ 0
↔ ¬ 0 < 2) |
| 10 | | pm2.21 123 |
. . . . . . . . . . . . . 14
⊢ (¬ 0
< 2 → (0 < 2 → 𝑥 ≠ ∅)) |
| 11 | 9, 10 | sylbi 217 |
. . . . . . . . . . . . 13
⊢ (2 ≤ 0
→ (0 < 2 → 𝑥
≠ ∅)) |
| 12 | 6, 11 | biimtrdi 253 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → (2 ≤
(♯‘𝑥) → (0
< 2 → 𝑥 ≠
∅))) |
| 13 | 12 | adantld 490 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤
(♯‘𝑥)) →
(0 < 2 → 𝑥 ≠
∅))) |
| 14 | 13 | impcomd 411 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((0 < 2
∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(♯‘𝑥))) →
𝑥 ≠
∅)) |
| 15 | | ax-1 6 |
. . . . . . . . . 10
⊢ (𝑥 ≠ ∅ → ((0 < 2
∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(♯‘𝑥))) →
𝑥 ≠
∅)) |
| 16 | 14, 15 | pm2.61ine 3025 |
. . . . . . . . 9
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(♯‘𝑥))) →
𝑥 ≠
∅) |
| 17 | | eldifsn 4786 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ↔
(𝑥 ∈ 𝒫 𝑉 ∧ 𝑥 ≠ ∅)) |
| 18 | 2, 16, 17 | sylanbrc 583 |
. . . . . . . 8
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(♯‘𝑥))) →
𝑥 ∈ (𝒫 𝑉 ∖
{∅})) |
| 19 | | simprr 773 |
. . . . . . . 8
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(♯‘𝑥))) →
2 ≤ (♯‘𝑥)) |
| 20 | 18, 19 | jca 511 |
. . . . . . 7
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(♯‘𝑥))) →
(𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 2 ≤
(♯‘𝑥))) |
| 21 | 20 | ex 412 |
. . . . . 6
⊢ (0 < 2
→ ((𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(♯‘𝑥)) →
(𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 2 ≤
(♯‘𝑥)))) |
| 22 | | eldifi 4131 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝑉 ∖ {∅}) → 𝑥 ∈ 𝒫 𝑉) |
| 23 | 22 | anim1i 615 |
. . . . . 6
⊢ ((𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 2 ≤
(♯‘𝑥)) →
(𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤
(♯‘𝑥))) |
| 24 | 21, 23 | impbid1 225 |
. . . . 5
⊢ (0 < 2
→ ((𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(♯‘𝑥)) ↔
(𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 2 ≤
(♯‘𝑥)))) |
| 25 | 24 | rabbidva2 3438 |
. . . 4
⊢ (0 < 2
→ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)} = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ 2
≤ (♯‘𝑥)}) |
| 26 | 1, 25 | ax-mp 5 |
. . 3
⊢ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤
(♯‘𝑥)} = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ 2
≤ (♯‘𝑥)} |
| 27 | 26 | ineq2i 4217 |
. 2
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∩ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)}) =
({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∩ {𝑥 ∈ (𝒫
𝑉 ∖ {∅})
∣ 2 ≤ (♯‘𝑥)}) |
| 28 | | inrab 4316 |
. 2
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∩ {𝑥 ∈ (𝒫
𝑉 ∖ {∅})
∣ 2 ≤ (♯‘𝑥)}) = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
((♯‘𝑥) ≤ 2
∧ 2 ≤ (♯‘𝑥))} |
| 29 | | hashxnn0 14378 |
. . . . . . 7
⊢ (𝑥 ∈ V →
(♯‘𝑥) ∈
ℕ0*) |
| 30 | 29 | elv 3485 |
. . . . . 6
⊢
(♯‘𝑥)
∈ ℕ0* |
| 31 | | xnn0xr 12604 |
. . . . . 6
⊢
((♯‘𝑥)
∈ ℕ0* → (♯‘𝑥) ∈
ℝ*) |
| 32 | 30, 31 | ax-mp 5 |
. . . . 5
⊢
(♯‘𝑥)
∈ ℝ* |
| 33 | 7 | rexri 11319 |
. . . . 5
⊢ 2 ∈
ℝ* |
| 34 | | xrletri3 13196 |
. . . . 5
⊢
(((♯‘𝑥)
∈ ℝ* ∧ 2 ∈ ℝ*) →
((♯‘𝑥) = 2
↔ ((♯‘𝑥)
≤ 2 ∧ 2 ≤ (♯‘𝑥)))) |
| 35 | 32, 33, 34 | mp2an 692 |
. . . 4
⊢
((♯‘𝑥) =
2 ↔ ((♯‘𝑥)
≤ 2 ∧ 2 ≤ (♯‘𝑥))) |
| 36 | 35 | bicomi 224 |
. . 3
⊢
(((♯‘𝑥)
≤ 2 ∧ 2 ≤ (♯‘𝑥)) ↔ (♯‘𝑥) = 2) |
| 37 | 36 | rabbii 3442 |
. 2
⊢ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
((♯‘𝑥) ≤ 2
∧ 2 ≤ (♯‘𝑥))} = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2} |
| 38 | 27, 28, 37 | 3eqtri 2769 |
1
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) ≤ 2}
∩ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(♯‘𝑥)}) =
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(♯‘𝑥) =
2} |