Step |
Hyp |
Ref |
Expression |
1 |
|
iscn |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ) ) ) |
2 |
|
f1oi |
⊢ ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋 |
3 |
|
f1of |
⊢ ( ( I ↾ 𝑋 ) : 𝑋 –1-1-onto→ 𝑋 → ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 ) |
4 |
2 3
|
ax-mp |
⊢ ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 |
5 |
4
|
biantrur |
⊢ ( ∀ 𝑥 ∈ 𝐾 ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ↔ ( ( I ↾ 𝑋 ) : 𝑋 ⟶ 𝑋 ∧ ∀ 𝑥 ∈ 𝐾 ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ) ) |
6 |
1 5
|
bitr4di |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ∀ 𝑥 ∈ 𝐾 ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ) ) |
7 |
|
cnvresid |
⊢ ◡ ( I ↾ 𝑋 ) = ( I ↾ 𝑋 ) |
8 |
7
|
imaeq1i |
⊢ ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) = ( ( I ↾ 𝑋 ) “ 𝑥 ) |
9 |
|
elssuni |
⊢ ( 𝑥 ∈ 𝐾 → 𝑥 ⊆ ∪ 𝐾 ) |
10 |
9
|
adantl |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ⊆ ∪ 𝐾 ) |
11 |
|
toponuni |
⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐾 ) |
12 |
11
|
ad2antlr |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝑋 = ∪ 𝐾 ) |
13 |
10 12
|
sseqtrrd |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐾 ) → 𝑥 ⊆ 𝑋 ) |
14 |
|
resiima |
⊢ ( 𝑥 ⊆ 𝑋 → ( ( I ↾ 𝑋 ) “ 𝑥 ) = 𝑥 ) |
15 |
13 14
|
syl |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( I ↾ 𝑋 ) “ 𝑥 ) = 𝑥 ) |
16 |
8 15
|
syl5eq |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) = 𝑥 ) |
17 |
16
|
eleq1d |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝑥 ∈ 𝐾 ) → ( ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ↔ 𝑥 ∈ 𝐽 ) ) |
18 |
17
|
ralbidva |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝐾 ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ 𝐾 𝑥 ∈ 𝐽 ) ) |
19 |
|
dfss3 |
⊢ ( 𝐾 ⊆ 𝐽 ↔ ∀ 𝑥 ∈ 𝐾 𝑥 ∈ 𝐽 ) |
20 |
18 19
|
bitr4di |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ∀ 𝑥 ∈ 𝐾 ( ◡ ( I ↾ 𝑋 ) “ 𝑥 ) ∈ 𝐽 ↔ 𝐾 ⊆ 𝐽 ) ) |
21 |
6 20
|
bitrd |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( I ↾ 𝑋 ) ∈ ( 𝐽 Cn 𝐾 ) ↔ 𝐾 ⊆ 𝐽 ) ) |