Step |
Hyp |
Ref |
Expression |
1 |
|
0ex |
⊢ ∅ ∈ V |
2 |
|
isust |
⊢ ( ∅ ∈ V → ( 𝑢 ∈ ( UnifOn ‘ ∅ ) ↔ ( 𝑢 ⊆ 𝒫 ( ∅ × ∅ ) ∧ ( ∅ × ∅ ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ ∅ ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) ) |
3 |
1 2
|
ax-mp |
⊢ ( 𝑢 ∈ ( UnifOn ‘ ∅ ) ↔ ( 𝑢 ⊆ 𝒫 ( ∅ × ∅ ) ∧ ( ∅ × ∅ ) ∈ 𝑢 ∧ ∀ 𝑣 ∈ 𝑢 ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ 𝑢 ) ∧ ∀ 𝑤 ∈ 𝑢 ( 𝑣 ∩ 𝑤 ) ∈ 𝑢 ∧ ( ( I ↾ ∅ ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ 𝑢 ∧ ∃ 𝑤 ∈ 𝑢 ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) |
4 |
3
|
simp1bi |
⊢ ( 𝑢 ∈ ( UnifOn ‘ ∅ ) → 𝑢 ⊆ 𝒫 ( ∅ × ∅ ) ) |
5 |
|
0xp |
⊢ ( ∅ × ∅ ) = ∅ |
6 |
5
|
pweqi |
⊢ 𝒫 ( ∅ × ∅ ) = 𝒫 ∅ |
7 |
|
pw0 |
⊢ 𝒫 ∅ = { ∅ } |
8 |
6 7
|
eqtri |
⊢ 𝒫 ( ∅ × ∅ ) = { ∅ } |
9 |
4 8
|
sseqtrdi |
⊢ ( 𝑢 ∈ ( UnifOn ‘ ∅ ) → 𝑢 ⊆ { ∅ } ) |
10 |
|
ustbasel |
⊢ ( 𝑢 ∈ ( UnifOn ‘ ∅ ) → ( ∅ × ∅ ) ∈ 𝑢 ) |
11 |
5 10
|
eqeltrrid |
⊢ ( 𝑢 ∈ ( UnifOn ‘ ∅ ) → ∅ ∈ 𝑢 ) |
12 |
11
|
snssd |
⊢ ( 𝑢 ∈ ( UnifOn ‘ ∅ ) → { ∅ } ⊆ 𝑢 ) |
13 |
9 12
|
eqssd |
⊢ ( 𝑢 ∈ ( UnifOn ‘ ∅ ) → 𝑢 = { ∅ } ) |
14 |
|
velsn |
⊢ ( 𝑢 ∈ { { ∅ } } ↔ 𝑢 = { ∅ } ) |
15 |
13 14
|
sylibr |
⊢ ( 𝑢 ∈ ( UnifOn ‘ ∅ ) → 𝑢 ∈ { { ∅ } } ) |
16 |
15
|
ssriv |
⊢ ( UnifOn ‘ ∅ ) ⊆ { { ∅ } } |
17 |
8
|
eqimss2i |
⊢ { ∅ } ⊆ 𝒫 ( ∅ × ∅ ) |
18 |
1
|
snid |
⊢ ∅ ∈ { ∅ } |
19 |
5 18
|
eqeltri |
⊢ ( ∅ × ∅ ) ∈ { ∅ } |
20 |
18
|
a1i |
⊢ ( ∅ ⊆ ∅ → ∅ ∈ { ∅ } ) |
21 |
8
|
raleqi |
⊢ ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ↔ ∀ 𝑤 ∈ { ∅ } ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ) |
22 |
|
sseq2 |
⊢ ( 𝑤 = ∅ → ( ∅ ⊆ 𝑤 ↔ ∅ ⊆ ∅ ) ) |
23 |
|
eleq1 |
⊢ ( 𝑤 = ∅ → ( 𝑤 ∈ { ∅ } ↔ ∅ ∈ { ∅ } ) ) |
24 |
22 23
|
imbi12d |
⊢ ( 𝑤 = ∅ → ( ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ↔ ( ∅ ⊆ ∅ → ∅ ∈ { ∅ } ) ) ) |
25 |
1 24
|
ralsn |
⊢ ( ∀ 𝑤 ∈ { ∅ } ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ↔ ( ∅ ⊆ ∅ → ∅ ∈ { ∅ } ) ) |
26 |
21 25
|
bitri |
⊢ ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ↔ ( ∅ ⊆ ∅ → ∅ ∈ { ∅ } ) ) |
27 |
20 26
|
mpbir |
⊢ ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) |
28 |
|
inidm |
⊢ ( ∅ ∩ ∅ ) = ∅ |
29 |
28 18
|
eqeltri |
⊢ ( ∅ ∩ ∅ ) ∈ { ∅ } |
30 |
|
ineq2 |
⊢ ( 𝑤 = ∅ → ( ∅ ∩ 𝑤 ) = ( ∅ ∩ ∅ ) ) |
31 |
30
|
eleq1d |
⊢ ( 𝑤 = ∅ → ( ( ∅ ∩ 𝑤 ) ∈ { ∅ } ↔ ( ∅ ∩ ∅ ) ∈ { ∅ } ) ) |
32 |
1 31
|
ralsn |
⊢ ( ∀ 𝑤 ∈ { ∅ } ( ∅ ∩ 𝑤 ) ∈ { ∅ } ↔ ( ∅ ∩ ∅ ) ∈ { ∅ } ) |
33 |
29 32
|
mpbir |
⊢ ∀ 𝑤 ∈ { ∅ } ( ∅ ∩ 𝑤 ) ∈ { ∅ } |
34 |
|
res0 |
⊢ ( I ↾ ∅ ) = ∅ |
35 |
34
|
eqimssi |
⊢ ( I ↾ ∅ ) ⊆ ∅ |
36 |
|
cnv0 |
⊢ ◡ ∅ = ∅ |
37 |
36 18
|
eqeltri |
⊢ ◡ ∅ ∈ { ∅ } |
38 |
|
0trrel |
⊢ ( ∅ ∘ ∅ ) ⊆ ∅ |
39 |
|
id |
⊢ ( 𝑤 = ∅ → 𝑤 = ∅ ) |
40 |
39 39
|
coeq12d |
⊢ ( 𝑤 = ∅ → ( 𝑤 ∘ 𝑤 ) = ( ∅ ∘ ∅ ) ) |
41 |
40
|
sseq1d |
⊢ ( 𝑤 = ∅ → ( ( 𝑤 ∘ 𝑤 ) ⊆ ∅ ↔ ( ∅ ∘ ∅ ) ⊆ ∅ ) ) |
42 |
1 41
|
rexsn |
⊢ ( ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ ∅ ↔ ( ∅ ∘ ∅ ) ⊆ ∅ ) |
43 |
38 42
|
mpbir |
⊢ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ ∅ |
44 |
35 37 43
|
3pm3.2i |
⊢ ( ( I ↾ ∅ ) ⊆ ∅ ∧ ◡ ∅ ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ ∅ ) |
45 |
|
sseq1 |
⊢ ( 𝑣 = ∅ → ( 𝑣 ⊆ 𝑤 ↔ ∅ ⊆ 𝑤 ) ) |
46 |
45
|
imbi1d |
⊢ ( 𝑣 = ∅ → ( ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ↔ ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ) ) |
47 |
46
|
ralbidv |
⊢ ( 𝑣 = ∅ → ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ↔ ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ) ) |
48 |
|
ineq1 |
⊢ ( 𝑣 = ∅ → ( 𝑣 ∩ 𝑤 ) = ( ∅ ∩ 𝑤 ) ) |
49 |
48
|
eleq1d |
⊢ ( 𝑣 = ∅ → ( ( 𝑣 ∩ 𝑤 ) ∈ { ∅ } ↔ ( ∅ ∩ 𝑤 ) ∈ { ∅ } ) ) |
50 |
49
|
ralbidv |
⊢ ( 𝑣 = ∅ → ( ∀ 𝑤 ∈ { ∅ } ( 𝑣 ∩ 𝑤 ) ∈ { ∅ } ↔ ∀ 𝑤 ∈ { ∅ } ( ∅ ∩ 𝑤 ) ∈ { ∅ } ) ) |
51 |
|
sseq2 |
⊢ ( 𝑣 = ∅ → ( ( I ↾ ∅ ) ⊆ 𝑣 ↔ ( I ↾ ∅ ) ⊆ ∅ ) ) |
52 |
|
cnveq |
⊢ ( 𝑣 = ∅ → ◡ 𝑣 = ◡ ∅ ) |
53 |
52
|
eleq1d |
⊢ ( 𝑣 = ∅ → ( ◡ 𝑣 ∈ { ∅ } ↔ ◡ ∅ ∈ { ∅ } ) ) |
54 |
|
sseq2 |
⊢ ( 𝑣 = ∅ → ( ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ↔ ( 𝑤 ∘ 𝑤 ) ⊆ ∅ ) ) |
55 |
54
|
rexbidv |
⊢ ( 𝑣 = ∅ → ( ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ↔ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ ∅ ) ) |
56 |
51 53 55
|
3anbi123d |
⊢ ( 𝑣 = ∅ → ( ( ( I ↾ ∅ ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ↔ ( ( I ↾ ∅ ) ⊆ ∅ ∧ ◡ ∅ ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ ∅ ) ) ) |
57 |
47 50 56
|
3anbi123d |
⊢ ( 𝑣 = ∅ → ( ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ∧ ∀ 𝑤 ∈ { ∅ } ( 𝑣 ∩ 𝑤 ) ∈ { ∅ } ∧ ( ( I ↾ ∅ ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ↔ ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ∧ ∀ 𝑤 ∈ { ∅ } ( ∅ ∩ 𝑤 ) ∈ { ∅ } ∧ ( ( I ↾ ∅ ) ⊆ ∅ ∧ ◡ ∅ ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ ∅ ) ) ) ) |
58 |
1 57
|
ralsn |
⊢ ( ∀ 𝑣 ∈ { ∅ } ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ∧ ∀ 𝑤 ∈ { ∅ } ( 𝑣 ∩ 𝑤 ) ∈ { ∅ } ∧ ( ( I ↾ ∅ ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ↔ ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( ∅ ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ∧ ∀ 𝑤 ∈ { ∅ } ( ∅ ∩ 𝑤 ) ∈ { ∅ } ∧ ( ( I ↾ ∅ ) ⊆ ∅ ∧ ◡ ∅ ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ ∅ ) ) ) |
59 |
27 33 44 58
|
mpbir3an |
⊢ ∀ 𝑣 ∈ { ∅ } ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ∧ ∀ 𝑤 ∈ { ∅ } ( 𝑣 ∩ 𝑤 ) ∈ { ∅ } ∧ ( ( I ↾ ∅ ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) |
60 |
|
isust |
⊢ ( ∅ ∈ V → ( { ∅ } ∈ ( UnifOn ‘ ∅ ) ↔ ( { ∅ } ⊆ 𝒫 ( ∅ × ∅ ) ∧ ( ∅ × ∅ ) ∈ { ∅ } ∧ ∀ 𝑣 ∈ { ∅ } ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ∧ ∀ 𝑤 ∈ { ∅ } ( 𝑣 ∩ 𝑤 ) ∈ { ∅ } ∧ ( ( I ↾ ∅ ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) ) |
61 |
1 60
|
ax-mp |
⊢ ( { ∅ } ∈ ( UnifOn ‘ ∅ ) ↔ ( { ∅ } ⊆ 𝒫 ( ∅ × ∅ ) ∧ ( ∅ × ∅ ) ∈ { ∅ } ∧ ∀ 𝑣 ∈ { ∅ } ( ∀ 𝑤 ∈ 𝒫 ( ∅ × ∅ ) ( 𝑣 ⊆ 𝑤 → 𝑤 ∈ { ∅ } ) ∧ ∀ 𝑤 ∈ { ∅ } ( 𝑣 ∩ 𝑤 ) ∈ { ∅ } ∧ ( ( I ↾ ∅ ) ⊆ 𝑣 ∧ ◡ 𝑣 ∈ { ∅ } ∧ ∃ 𝑤 ∈ { ∅ } ( 𝑤 ∘ 𝑤 ) ⊆ 𝑣 ) ) ) ) |
62 |
17 19 59 61
|
mpbir3an |
⊢ { ∅ } ∈ ( UnifOn ‘ ∅ ) |
63 |
|
snssi |
⊢ ( { ∅ } ∈ ( UnifOn ‘ ∅ ) → { { ∅ } } ⊆ ( UnifOn ‘ ∅ ) ) |
64 |
62 63
|
ax-mp |
⊢ { { ∅ } } ⊆ ( UnifOn ‘ ∅ ) |
65 |
16 64
|
eqssi |
⊢ ( UnifOn ‘ ∅ ) = { { ∅ } } |