Proof of Theorem umgrislfupgrlem
Step | Hyp | Ref
| Expression |
1 | | 2pos 10989 |
. . . 4
⊢ 0 <
2 |
2 | | simprl 790 |
. . . . . . . . 9
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥))) → 𝑥 ∈ 𝒫 𝑉) |
3 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = ∅ → (#‘𝑥) =
(#‘∅)) |
4 | | hash0 13019 |
. . . . . . . . . . . . . . . 16
⊢
(#‘∅) = 0 |
5 | 3, 4 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∅ → (#‘𝑥) = 0) |
6 | 5 | breq2d 4595 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∅ → (2 ≤
(#‘𝑥) ↔ 2 ≤
0)) |
7 | | 2re 10967 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ |
8 | | 0re 9919 |
. . . . . . . . . . . . . . . 16
⊢ 0 ∈
ℝ |
9 | 7, 8 | lenlti 10036 |
. . . . . . . . . . . . . . 15
⊢ (2 ≤ 0
↔ ¬ 0 < 2) |
10 | | pm2.21 119 |
. . . . . . . . . . . . . . 15
⊢ (¬ 0
< 2 → (0 < 2 → 𝑥 ≠ ∅)) |
11 | 9, 10 | sylbi 206 |
. . . . . . . . . . . . . 14
⊢ (2 ≤ 0
→ (0 < 2 → 𝑥
≠ ∅)) |
12 | 6, 11 | syl6bi 242 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∅ → (2 ≤
(#‘𝑥) → (0 <
2 → 𝑥 ≠
∅))) |
13 | 12 | adantld 482 |
. . . . . . . . . . . 12
⊢ (𝑥 = ∅ → ((𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ (#‘𝑥)) → (0 < 2 → 𝑥 ≠
∅))) |
14 | 13 | com23 84 |
. . . . . . . . . . 11
⊢ (𝑥 = ∅ → (0 < 2
→ ((𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥)) → 𝑥 ≠
∅))) |
15 | 14 | impd 446 |
. . . . . . . . . 10
⊢ (𝑥 = ∅ → ((0 < 2
∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥))) → 𝑥 ≠ ∅)) |
16 | | ax-1 6 |
. . . . . . . . . 10
⊢ (𝑥 ≠ ∅ → ((0 < 2
∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥))) → 𝑥 ≠ ∅)) |
17 | 15, 16 | pm2.61ine 2865 |
. . . . . . . . 9
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥))) → 𝑥 ≠ ∅) |
18 | | eldifsn 4260 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ↔
(𝑥 ∈ 𝒫 𝑉 ∧ 𝑥 ≠ ∅)) |
19 | 2, 17, 18 | sylanbrc 695 |
. . . . . . . 8
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥))) → 𝑥 ∈ (𝒫 𝑉 ∖
{∅})) |
20 | | simprr 792 |
. . . . . . . 8
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥))) → 2 ≤
(#‘𝑥)) |
21 | 19, 20 | jca 553 |
. . . . . . 7
⊢ ((0 <
2 ∧ (𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥))) → (𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 2 ≤
(#‘𝑥))) |
22 | 21 | ex 449 |
. . . . . 6
⊢ (0 < 2
→ ((𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥)) → (𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 2 ≤
(#‘𝑥)))) |
23 | | eldifi 3694 |
. . . . . . 7
⊢ (𝑥 ∈ (𝒫 𝑉 ∖ {∅}) → 𝑥 ∈ 𝒫 𝑉) |
24 | 23 | anim1i 590 |
. . . . . 6
⊢ ((𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 2 ≤
(#‘𝑥)) → (𝑥 ∈ 𝒫 𝑉 ∧ 2 ≤ (#‘𝑥))) |
25 | 22, 24 | impbid1 214 |
. . . . 5
⊢ (0 < 2
→ ((𝑥 ∈ 𝒫
𝑉 ∧ 2 ≤
(#‘𝑥)) ↔ (𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∧ 2 ≤
(#‘𝑥)))) |
26 | 25 | rabbidva2 3162 |
. . . 4
⊢ (0 < 2
→ {𝑥 ∈ 𝒫
𝑉 ∣ 2 ≤
(#‘𝑥)} = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ 2
≤ (#‘𝑥)}) |
27 | 1, 26 | ax-mp 5 |
. . 3
⊢ {𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)} = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ 2 ≤
(#‘𝑥)} |
28 | 27 | ineq2i 3773 |
. 2
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∩
{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)}) = ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) ≤ 2} ∩ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ 2
≤ (#‘𝑥)}) |
29 | | inrab 3858 |
. 2
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∩
{𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ 2
≤ (#‘𝑥)}) = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
((#‘𝑥) ≤ 2 ∧ 2
≤ (#‘𝑥))} |
30 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
31 | | hashxnn0 12989 |
. . . . . . . 8
⊢ (𝑥 ∈ V → (#‘𝑥) ∈
ℕ0*) |
32 | 30, 31 | ax-mp 5 |
. . . . . . 7
⊢
(#‘𝑥) ∈
ℕ0* |
33 | | xnn0xr 11245 |
. . . . . . 7
⊢
((#‘𝑥) ∈
ℕ0* → (#‘𝑥) ∈
ℝ*) |
34 | 32, 33 | ax-mp 5 |
. . . . . 6
⊢
(#‘𝑥) ∈
ℝ* |
35 | 7 | rexri 9976 |
. . . . . 6
⊢ 2 ∈
ℝ* |
36 | | xrletri3 11861 |
. . . . . 6
⊢
(((#‘𝑥) ∈
ℝ* ∧ 2 ∈ ℝ*) → ((#‘𝑥) = 2 ↔ ((#‘𝑥) ≤ 2 ∧ 2 ≤
(#‘𝑥)))) |
37 | 34, 35, 36 | mp2an 704 |
. . . . 5
⊢
((#‘𝑥) = 2
↔ ((#‘𝑥) ≤ 2
∧ 2 ≤ (#‘𝑥))) |
38 | 37 | bicomi 213 |
. . . 4
⊢
(((#‘𝑥) ≤ 2
∧ 2 ≤ (#‘𝑥))
↔ (#‘𝑥) =
2) |
39 | 38 | a1i 11 |
. . 3
⊢ (𝑥 ∈ (𝒫 𝑉 ∖ {∅}) →
(((#‘𝑥) ≤ 2 ∧
2 ≤ (#‘𝑥)) ↔
(#‘𝑥) =
2)) |
40 | 39 | rabbiia 3161 |
. 2
⊢ {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
((#‘𝑥) ≤ 2 ∧ 2
≤ (#‘𝑥))} = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) =
2} |
41 | 28, 29, 40 | 3eqtri 2636 |
1
⊢ ({𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣
(#‘𝑥) ≤ 2} ∩
{𝑥 ∈ 𝒫 𝑉 ∣ 2 ≤ (#‘𝑥)}) = {𝑥 ∈ (𝒫 𝑉 ∖ {∅}) ∣ (#‘𝑥) = 2} |