Step |
Hyp |
Ref |
Expression |
1 |
|
cntop1 |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top ) |
2 |
1
|
3ad2ant3 |
⊢ ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Top ) |
3 |
|
simpl3 |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) |
4 |
|
cnima |
⊢ ( ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ∧ 𝑤 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑤 ) ∈ 𝐽 ) |
5 |
3 4
|
sylan |
⊢ ( ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ◡ 𝐹 “ 𝑤 ) ∈ 𝐽 ) |
6 |
|
eleq2 |
⊢ ( 𝑧 = ( ◡ 𝐹 “ 𝑤 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ) |
7 |
|
eleq2 |
⊢ ( 𝑧 = ( ◡ 𝐹 “ 𝑤 ) → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ) |
8 |
6 7
|
bibi12d |
⊢ ( 𝑧 = ( ◡ 𝐹 “ 𝑤 ) → ( ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ) ) |
9 |
8
|
rspcv |
⊢ ( ( ◡ 𝐹 “ 𝑤 ) ∈ 𝐽 → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ) ) |
10 |
5 9
|
syl |
⊢ ( ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ) ) |
11 |
|
simprl |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝑥 ∈ ∪ 𝐽 ) |
12 |
|
eqid |
⊢ ∪ 𝐽 = ∪ 𝐽 |
13 |
|
eqid |
⊢ ∪ 𝐾 = ∪ 𝐾 |
14 |
12 13
|
cnf |
⊢ ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ) |
15 |
3 14
|
syl |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐹 : ∪ 𝐽 ⟶ ∪ 𝐾 ) |
16 |
15
|
ffnd |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐹 Fn ∪ 𝐽 ) |
17 |
|
elpreima |
⊢ ( 𝐹 Fn ∪ 𝐽 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ) ) ) |
18 |
16 17
|
syl |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝑥 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ) ) ) |
19 |
11 18
|
mpbirand |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ) ) |
20 |
|
simprr |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝑦 ∈ ∪ 𝐽 ) |
21 |
|
elpreima |
⊢ ( 𝐹 Fn ∪ 𝐽 → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝑦 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) ) |
22 |
16 21
|
syl |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝑦 ∈ ∪ 𝐽 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) ) |
23 |
20 22
|
mpbirand |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) |
24 |
19 23
|
bibi12d |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) ) |
25 |
24
|
adantr |
⊢ ( ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑤 ) ↔ 𝑦 ∈ ( ◡ 𝐹 “ 𝑤 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) ) |
26 |
10 25
|
sylibd |
⊢ ( ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) ∧ 𝑤 ∈ 𝐾 ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) ) |
27 |
26
|
ralrimdva |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ∀ 𝑤 ∈ 𝐾 ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) ) ) |
28 |
|
simpl1 |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐾 ∈ Kol2 ) |
29 |
15 11
|
ffvelrnd |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝐾 ) |
30 |
15 20
|
ffvelrnd |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐾 ) |
31 |
13
|
t0sep |
⊢ ( ( 𝐾 ∈ Kol2 ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝐾 ∧ ( 𝐹 ‘ 𝑦 ) ∈ ∪ 𝐾 ) ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) |
32 |
28 29 30 31
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ∀ 𝑤 ∈ 𝐾 ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑤 ↔ ( 𝐹 ‘ 𝑦 ) ∈ 𝑤 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) |
33 |
27 32
|
syld |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) |
34 |
|
simpl2 |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝐹 : 𝑋 –1-1→ 𝑌 ) |
35 |
15
|
fdmd |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → dom 𝐹 = ∪ 𝐽 ) |
36 |
|
f1dm |
⊢ ( 𝐹 : 𝑋 –1-1→ 𝑌 → dom 𝐹 = 𝑋 ) |
37 |
34 36
|
syl |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → dom 𝐹 = 𝑋 ) |
38 |
35 37
|
eqtr3d |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ∪ 𝐽 = 𝑋 ) |
39 |
11 38
|
eleqtrd |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝑥 ∈ 𝑋 ) |
40 |
20 38
|
eleqtrd |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → 𝑦 ∈ 𝑋 ) |
41 |
|
f1fveq |
⊢ ( ( 𝐹 : 𝑋 –1-1→ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) ) |
42 |
34 39 40 41
|
syl12anc |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ 𝑥 = 𝑦 ) ) |
43 |
33 42
|
sylibd |
⊢ ( ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) ∧ ( 𝑥 ∈ ∪ 𝐽 ∧ 𝑦 ∈ ∪ 𝐽 ) ) → ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) ) |
44 |
43
|
ralrimivva |
⊢ ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) ) |
45 |
12
|
ist0 |
⊢ ( 𝐽 ∈ Kol2 ↔ ( 𝐽 ∈ Top ∧ ∀ 𝑥 ∈ ∪ 𝐽 ∀ 𝑦 ∈ ∪ 𝐽 ( ∀ 𝑧 ∈ 𝐽 ( 𝑥 ∈ 𝑧 ↔ 𝑦 ∈ 𝑧 ) → 𝑥 = 𝑦 ) ) ) |
46 |
2 44 45
|
sylanbrc |
⊢ ( ( 𝐾 ∈ Kol2 ∧ 𝐹 : 𝑋 –1-1→ 𝑌 ∧ 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ) → 𝐽 ∈ Kol2 ) |