Step |
Hyp |
Ref |
Expression |
1 |
|
cnextfval.1 |
⊢ 𝑋 = ∪ 𝐽 |
2 |
|
cnextfval.2 |
⊢ 𝐵 = ∪ 𝐾 |
3 |
|
cnextval |
⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 CnExt 𝐾 ) = ( 𝑓 ∈ ( ∪ 𝐾 ↑pm ∪ 𝐽 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) ) |
4 |
3
|
adantr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) → ( 𝐽 CnExt 𝐾 ) = ( 𝑓 ∈ ( ∪ 𝐾 ↑pm ∪ 𝐽 ) ↦ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) ) ) |
5 |
|
simpr |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 ) |
6 |
5
|
dmeqd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = dom 𝐹 ) |
7 |
|
simplrl |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
8 |
7
|
fdmd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → dom 𝐹 = 𝐴 ) |
9 |
6 8
|
eqtrd |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → dom 𝑓 = 𝐴 ) |
10 |
9
|
fveq2d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) = ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ) |
11 |
9
|
oveq2d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) = ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) |
12 |
11
|
oveq2d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) = ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ) |
13 |
12 5
|
fveq12d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) = ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) |
14 |
13
|
xpeq2d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) = ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
15 |
10 14
|
iuneq12d |
⊢ ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) ∧ 𝑓 = 𝐹 ) → ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ dom 𝑓 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t dom 𝑓 ) ) ‘ 𝑓 ) ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |
16 |
|
uniexg |
⊢ ( 𝐾 ∈ Top → ∪ 𝐾 ∈ V ) |
17 |
16
|
ad2antlr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) → ∪ 𝐾 ∈ V ) |
18 |
|
uniexg |
⊢ ( 𝐽 ∈ Top → ∪ 𝐽 ∈ V ) |
19 |
18
|
ad2antrr |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) → ∪ 𝐽 ∈ V ) |
20 |
|
eqid |
⊢ 𝐴 = 𝐴 |
21 |
20 2
|
feq23i |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 ↔ 𝐹 : 𝐴 ⟶ ∪ 𝐾 ) |
22 |
21
|
biimpi |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 ⟶ ∪ 𝐾 ) |
23 |
22
|
ad2antrl |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) → 𝐹 : 𝐴 ⟶ ∪ 𝐾 ) |
24 |
1
|
sseq2i |
⊢ ( 𝐴 ⊆ 𝑋 ↔ 𝐴 ⊆ ∪ 𝐽 ) |
25 |
24
|
biimpi |
⊢ ( 𝐴 ⊆ 𝑋 → 𝐴 ⊆ ∪ 𝐽 ) |
26 |
25
|
ad2antll |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) → 𝐴 ⊆ ∪ 𝐽 ) |
27 |
|
elpm2r |
⊢ ( ( ( ∪ 𝐾 ∈ V ∧ ∪ 𝐽 ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ∪ 𝐾 ∧ 𝐴 ⊆ ∪ 𝐽 ) ) → 𝐹 ∈ ( ∪ 𝐾 ↑pm ∪ 𝐽 ) ) |
28 |
17 19 23 26 27
|
syl22anc |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) → 𝐹 ∈ ( ∪ 𝐾 ↑pm ∪ 𝐽 ) ) |
29 |
|
fvex |
⊢ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ∈ V |
30 |
|
snex |
⊢ { 𝑥 } ∈ V |
31 |
|
fvex |
⊢ ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ∈ V |
32 |
30 31
|
xpex |
⊢ ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ∈ V |
33 |
29 32
|
iunex |
⊢ ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ∈ V |
34 |
33
|
a1i |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) → ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ∈ V ) |
35 |
4 15 28 34
|
fvmptd |
⊢ ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ⊆ 𝑋 ) ) → ( ( 𝐽 CnExt 𝐾 ) ‘ 𝐹 ) = ∪ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝐾 fLimf ( ( ( nei ‘ 𝐽 ) ‘ { 𝑥 } ) ↾t 𝐴 ) ) ‘ 𝐹 ) ) ) |