Step | Hyp | Ref
| Expression |
1 | | 0ex 5172 |
. . . . . . . 8
⊢ ∅
∈ V |
2 | | isust 22948 |
. . . . . . . 8
⊢ (∅
∈ V → (𝑢 ∈
(UnifOn‘∅) ↔ (𝑢 ⊆ 𝒫 (∅ × ∅)
∧ (∅ × ∅) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (∅ ×
∅)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ ∅) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣))))) |
3 | 1, 2 | ax-mp 5 |
. . . . . . 7
⊢ (𝑢 ∈ (UnifOn‘∅)
↔ (𝑢 ⊆ 𝒫
(∅ × ∅) ∧ (∅ × ∅) ∈ 𝑢 ∧ ∀𝑣 ∈ 𝑢 (∀𝑤 ∈ 𝒫 (∅ ×
∅)(𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢) ∧ ∀𝑤 ∈ 𝑢 (𝑣 ∩ 𝑤) ∈ 𝑢 ∧ (( I ↾ ∅) ⊆ 𝑣 ∧ ◡𝑣 ∈ 𝑢 ∧ ∃𝑤 ∈ 𝑢 (𝑤 ∘ 𝑤) ⊆ 𝑣)))) |
4 | 3 | simp1bi 1146 |
. . . . . 6
⊢ (𝑢 ∈ (UnifOn‘∅)
→ 𝑢 ⊆ 𝒫
(∅ × ∅)) |
5 | | 0xp 5614 |
. . . . . . . 8
⊢ (∅
× ∅) = ∅ |
6 | 5 | pweqi 4503 |
. . . . . . 7
⊢ 𝒫
(∅ × ∅) = 𝒫 ∅ |
7 | | pw0 4697 |
. . . . . . 7
⊢ 𝒫
∅ = {∅} |
8 | 6, 7 | eqtri 2761 |
. . . . . 6
⊢ 𝒫
(∅ × ∅) = {∅} |
9 | 4, 8 | sseqtrdi 3925 |
. . . . 5
⊢ (𝑢 ∈ (UnifOn‘∅)
→ 𝑢 ⊆
{∅}) |
10 | | ustbasel 22951 |
. . . . . . 7
⊢ (𝑢 ∈ (UnifOn‘∅)
→ (∅ × ∅) ∈ 𝑢) |
11 | 5, 10 | eqeltrrid 2838 |
. . . . . 6
⊢ (𝑢 ∈ (UnifOn‘∅)
→ ∅ ∈ 𝑢) |
12 | 11 | snssd 4694 |
. . . . 5
⊢ (𝑢 ∈ (UnifOn‘∅)
→ {∅} ⊆ 𝑢) |
13 | 9, 12 | eqssd 3892 |
. . . 4
⊢ (𝑢 ∈ (UnifOn‘∅)
→ 𝑢 =
{∅}) |
14 | | velsn 4529 |
. . . 4
⊢ (𝑢 ∈ {{∅}} ↔ 𝑢 = {∅}) |
15 | 13, 14 | sylibr 237 |
. . 3
⊢ (𝑢 ∈ (UnifOn‘∅)
→ 𝑢 ∈
{{∅}}) |
16 | 15 | ssriv 3879 |
. 2
⊢
(UnifOn‘∅) ⊆ {{∅}} |
17 | 8 | eqimss2i 3934 |
. . . 4
⊢ {∅}
⊆ 𝒫 (∅ × ∅) |
18 | 1 | snid 4549 |
. . . . 5
⊢ ∅
∈ {∅} |
19 | 5, 18 | eqeltri 2829 |
. . . 4
⊢ (∅
× ∅) ∈ {∅} |
20 | 18 | a1i 11 |
. . . . . 6
⊢ (∅
⊆ ∅ → ∅ ∈ {∅}) |
21 | 8 | raleqi 3313 |
. . . . . . 7
⊢
(∀𝑤 ∈
𝒫 (∅ × ∅)(∅ ⊆ 𝑤 → 𝑤 ∈ {∅}) ↔ ∀𝑤 ∈ {∅} (∅
⊆ 𝑤 → 𝑤 ∈
{∅})) |
22 | | sseq2 3901 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (∅
⊆ 𝑤 ↔ ∅
⊆ ∅)) |
23 | | eleq1 2820 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑤 ∈ {∅} ↔ ∅
∈ {∅})) |
24 | 22, 23 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑤 = ∅ → ((∅
⊆ 𝑤 → 𝑤 ∈ {∅}) ↔
(∅ ⊆ ∅ → ∅ ∈ {∅}))) |
25 | 1, 24 | ralsn 4569 |
. . . . . . 7
⊢
(∀𝑤 ∈
{∅} (∅ ⊆ 𝑤 → 𝑤 ∈ {∅}) ↔ (∅ ⊆
∅ → ∅ ∈ {∅})) |
26 | 21, 25 | bitri 278 |
. . . . . 6
⊢
(∀𝑤 ∈
𝒫 (∅ × ∅)(∅ ⊆ 𝑤 → 𝑤 ∈ {∅}) ↔ (∅ ⊆
∅ → ∅ ∈ {∅})) |
27 | 20, 26 | mpbir 234 |
. . . . 5
⊢
∀𝑤 ∈
𝒫 (∅ × ∅)(∅ ⊆ 𝑤 → 𝑤 ∈ {∅}) |
28 | | inidm 4107 |
. . . . . . 7
⊢ (∅
∩ ∅) = ∅ |
29 | 28, 18 | eqeltri 2829 |
. . . . . 6
⊢ (∅
∩ ∅) ∈ {∅} |
30 | | ineq2 4095 |
. . . . . . . 8
⊢ (𝑤 = ∅ → (∅ ∩
𝑤) = (∅ ∩
∅)) |
31 | 30 | eleq1d 2817 |
. . . . . . 7
⊢ (𝑤 = ∅ → ((∅
∩ 𝑤) ∈ {∅}
↔ (∅ ∩ ∅) ∈ {∅})) |
32 | 1, 31 | ralsn 4569 |
. . . . . 6
⊢
(∀𝑤 ∈
{∅} (∅ ∩ 𝑤)
∈ {∅} ↔ (∅ ∩ ∅) ∈
{∅}) |
33 | 29, 32 | mpbir 234 |
. . . . 5
⊢
∀𝑤 ∈
{∅} (∅ ∩ 𝑤)
∈ {∅} |
34 | | res0 5823 |
. . . . . . 7
⊢ ( I
↾ ∅) = ∅ |
35 | 34 | eqimssi 3933 |
. . . . . 6
⊢ ( I
↾ ∅) ⊆ ∅ |
36 | | cnv0 5967 |
. . . . . . 7
⊢ ◡∅ = ∅ |
37 | 36, 18 | eqeltri 2829 |
. . . . . 6
⊢ ◡∅ ∈ {∅} |
38 | | 0trrel 14423 |
. . . . . . 7
⊢ (∅
∘ ∅) ⊆ ∅ |
39 | | id 22 |
. . . . . . . . . 10
⊢ (𝑤 = ∅ → 𝑤 = ∅) |
40 | 39, 39 | coeq12d 5701 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → (𝑤 ∘ 𝑤) = (∅ ∘
∅)) |
41 | 40 | sseq1d 3906 |
. . . . . . . 8
⊢ (𝑤 = ∅ → ((𝑤 ∘ 𝑤) ⊆ ∅ ↔ (∅ ∘
∅) ⊆ ∅)) |
42 | 1, 41 | rexsn 4570 |
. . . . . . 7
⊢
(∃𝑤 ∈
{∅} (𝑤 ∘ 𝑤) ⊆ ∅ ↔
(∅ ∘ ∅) ⊆ ∅) |
43 | 38, 42 | mpbir 234 |
. . . . . 6
⊢
∃𝑤 ∈
{∅} (𝑤 ∘ 𝑤) ⊆
∅ |
44 | 35, 37, 43 | 3pm3.2i 1340 |
. . . . 5
⊢ (( I
↾ ∅) ⊆ ∅ ∧ ◡∅ ∈ {∅} ∧ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ ∅) |
45 | | sseq1 3900 |
. . . . . . . . 9
⊢ (𝑣 = ∅ → (𝑣 ⊆ 𝑤 ↔ ∅ ⊆ 𝑤)) |
46 | 45 | imbi1d 345 |
. . . . . . . 8
⊢ (𝑣 = ∅ → ((𝑣 ⊆ 𝑤 → 𝑤 ∈ {∅}) ↔ (∅ ⊆
𝑤 → 𝑤 ∈ {∅}))) |
47 | 46 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑣 = ∅ → (∀𝑤 ∈ 𝒫 (∅
× ∅)(𝑣 ⊆
𝑤 → 𝑤 ∈ {∅}) ↔ ∀𝑤 ∈ 𝒫 (∅
× ∅)(∅ ⊆ 𝑤 → 𝑤 ∈ {∅}))) |
48 | | ineq1 4094 |
. . . . . . . . 9
⊢ (𝑣 = ∅ → (𝑣 ∩ 𝑤) = (∅ ∩ 𝑤)) |
49 | 48 | eleq1d 2817 |
. . . . . . . 8
⊢ (𝑣 = ∅ → ((𝑣 ∩ 𝑤) ∈ {∅} ↔ (∅ ∩
𝑤) ∈
{∅})) |
50 | 49 | ralbidv 3109 |
. . . . . . 7
⊢ (𝑣 = ∅ → (∀𝑤 ∈ {∅} (𝑣 ∩ 𝑤) ∈ {∅} ↔ ∀𝑤 ∈ {∅} (∅ ∩
𝑤) ∈
{∅})) |
51 | | sseq2 3901 |
. . . . . . . 8
⊢ (𝑣 = ∅ → (( I ↾
∅) ⊆ 𝑣 ↔ (
I ↾ ∅) ⊆ ∅)) |
52 | | cnveq 5710 |
. . . . . . . . 9
⊢ (𝑣 = ∅ → ◡𝑣 = ◡∅) |
53 | 52 | eleq1d 2817 |
. . . . . . . 8
⊢ (𝑣 = ∅ → (◡𝑣 ∈ {∅} ↔ ◡∅ ∈ {∅})) |
54 | | sseq2 3901 |
. . . . . . . . 9
⊢ (𝑣 = ∅ → ((𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ (𝑤 ∘ 𝑤) ⊆ ∅)) |
55 | 54 | rexbidv 3206 |
. . . . . . . 8
⊢ (𝑣 = ∅ → (∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ 𝑣 ↔ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ ∅)) |
56 | 51, 53, 55 | 3anbi123d 1437 |
. . . . . . 7
⊢ (𝑣 = ∅ → ((( I ↾
∅) ⊆ 𝑣 ∧
◡𝑣 ∈ {∅} ∧ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ 𝑣) ↔ (( I ↾ ∅) ⊆
∅ ∧ ◡∅ ∈ {∅}
∧ ∃𝑤 ∈
{∅} (𝑤 ∘ 𝑤) ⊆
∅))) |
57 | 47, 50, 56 | 3anbi123d 1437 |
. . . . . 6
⊢ (𝑣 = ∅ →
((∀𝑤 ∈
𝒫 (∅ × ∅)(𝑣 ⊆ 𝑤 → 𝑤 ∈ {∅}) ∧ ∀𝑤 ∈ {∅} (𝑣 ∩ 𝑤) ∈ {∅} ∧ (( I ↾
∅) ⊆ 𝑣 ∧
◡𝑣 ∈ {∅} ∧ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ 𝑣)) ↔ (∀𝑤 ∈ 𝒫 (∅ ×
∅)(∅ ⊆ 𝑤
→ 𝑤 ∈ {∅})
∧ ∀𝑤 ∈
{∅} (∅ ∩ 𝑤)
∈ {∅} ∧ (( I ↾ ∅) ⊆ ∅ ∧ ◡∅ ∈ {∅} ∧ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ ∅)))) |
58 | 1, 57 | ralsn 4569 |
. . . . 5
⊢
(∀𝑣 ∈
{∅} (∀𝑤 ∈
𝒫 (∅ × ∅)(𝑣 ⊆ 𝑤 → 𝑤 ∈ {∅}) ∧ ∀𝑤 ∈ {∅} (𝑣 ∩ 𝑤) ∈ {∅} ∧ (( I ↾
∅) ⊆ 𝑣 ∧
◡𝑣 ∈ {∅} ∧ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ 𝑣)) ↔ (∀𝑤 ∈ 𝒫 (∅ ×
∅)(∅ ⊆ 𝑤
→ 𝑤 ∈ {∅})
∧ ∀𝑤 ∈
{∅} (∅ ∩ 𝑤)
∈ {∅} ∧ (( I ↾ ∅) ⊆ ∅ ∧ ◡∅ ∈ {∅} ∧ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ ∅))) |
59 | 27, 33, 44, 58 | mpbir3an 1342 |
. . . 4
⊢
∀𝑣 ∈
{∅} (∀𝑤 ∈
𝒫 (∅ × ∅)(𝑣 ⊆ 𝑤 → 𝑤 ∈ {∅}) ∧ ∀𝑤 ∈ {∅} (𝑣 ∩ 𝑤) ∈ {∅} ∧ (( I ↾
∅) ⊆ 𝑣 ∧
◡𝑣 ∈ {∅} ∧ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ 𝑣)) |
60 | | isust 22948 |
. . . . 5
⊢ (∅
∈ V → ({∅} ∈ (UnifOn‘∅) ↔ ({∅}
⊆ 𝒫 (∅ × ∅) ∧ (∅ × ∅)
∈ {∅} ∧ ∀𝑣 ∈ {∅} (∀𝑤 ∈ 𝒫 (∅ ×
∅)(𝑣 ⊆ 𝑤 → 𝑤 ∈ {∅}) ∧ ∀𝑤 ∈ {∅} (𝑣 ∩ 𝑤) ∈ {∅} ∧ (( I ↾
∅) ⊆ 𝑣 ∧
◡𝑣 ∈ {∅} ∧ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ 𝑣))))) |
61 | 1, 60 | ax-mp 5 |
. . . 4
⊢
({∅} ∈ (UnifOn‘∅) ↔ ({∅} ⊆
𝒫 (∅ × ∅) ∧ (∅ × ∅) ∈
{∅} ∧ ∀𝑣
∈ {∅} (∀𝑤
∈ 𝒫 (∅ × ∅)(𝑣 ⊆ 𝑤 → 𝑤 ∈ {∅}) ∧ ∀𝑤 ∈ {∅} (𝑣 ∩ 𝑤) ∈ {∅} ∧ (( I ↾
∅) ⊆ 𝑣 ∧
◡𝑣 ∈ {∅} ∧ ∃𝑤 ∈ {∅} (𝑤 ∘ 𝑤) ⊆ 𝑣)))) |
62 | 17, 19, 59, 61 | mpbir3an 1342 |
. . 3
⊢ {∅}
∈ (UnifOn‘∅) |
63 | | snssi 4693 |
. . 3
⊢
({∅} ∈ (UnifOn‘∅) → {{∅}} ⊆
(UnifOn‘∅)) |
64 | 62, 63 | ax-mp 5 |
. 2
⊢
{{∅}} ⊆ (UnifOn‘∅) |
65 | 16, 64 | eqssi 3891 |
1
⊢
(UnifOn‘∅) = {{∅}} |