Step |
Hyp |
Ref |
Expression |
1 |
|
2ndcctbss.1 |
⊢ 𝐽 = ( topGen ‘ 𝐵 ) |
2 |
|
2ndcctbss.2 |
⊢ 𝑆 = { 〈 𝑢 , 𝑣 〉 ∣ ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) } |
3 |
|
simpr |
⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) → 𝐽 ∈ 2ndω ) |
4 |
|
is2ndc |
⊢ ( 𝐽 ∈ 2ndω ↔ ∃ 𝑐 ∈ TopBases ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) |
5 |
3 4
|
sylib |
⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) → ∃ 𝑐 ∈ TopBases ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) |
6 |
|
vex |
⊢ 𝑐 ∈ V |
7 |
6 6
|
xpex |
⊢ ( 𝑐 × 𝑐 ) ∈ V |
8 |
|
3simpa |
⊢ ( ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) → ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ) ) |
9 |
8
|
ssopab2i |
⊢ { 〈 𝑢 , 𝑣 〉 ∣ ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) } ⊆ { 〈 𝑢 , 𝑣 〉 ∣ ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ) } |
10 |
|
df-xp |
⊢ ( 𝑐 × 𝑐 ) = { 〈 𝑢 , 𝑣 〉 ∣ ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ) } |
11 |
9 2 10
|
3sstr4i |
⊢ 𝑆 ⊆ ( 𝑐 × 𝑐 ) |
12 |
|
ssdomg |
⊢ ( ( 𝑐 × 𝑐 ) ∈ V → ( 𝑆 ⊆ ( 𝑐 × 𝑐 ) → 𝑆 ≼ ( 𝑐 × 𝑐 ) ) ) |
13 |
7 11 12
|
mp2 |
⊢ 𝑆 ≼ ( 𝑐 × 𝑐 ) |
14 |
6
|
xpdom1 |
⊢ ( 𝑐 ≼ ω → ( 𝑐 × 𝑐 ) ≼ ( ω × 𝑐 ) ) |
15 |
|
omex |
⊢ ω ∈ V |
16 |
15
|
xpdom2 |
⊢ ( 𝑐 ≼ ω → ( ω × 𝑐 ) ≼ ( ω × ω ) ) |
17 |
|
domtr |
⊢ ( ( ( 𝑐 × 𝑐 ) ≼ ( ω × 𝑐 ) ∧ ( ω × 𝑐 ) ≼ ( ω × ω ) ) → ( 𝑐 × 𝑐 ) ≼ ( ω × ω ) ) |
18 |
14 16 17
|
syl2anc |
⊢ ( 𝑐 ≼ ω → ( 𝑐 × 𝑐 ) ≼ ( ω × ω ) ) |
19 |
|
xpomen |
⊢ ( ω × ω ) ≈ ω |
20 |
|
domentr |
⊢ ( ( ( 𝑐 × 𝑐 ) ≼ ( ω × ω ) ∧ ( ω × ω ) ≈ ω ) → ( 𝑐 × 𝑐 ) ≼ ω ) |
21 |
18 19 20
|
sylancl |
⊢ ( 𝑐 ≼ ω → ( 𝑐 × 𝑐 ) ≼ ω ) |
22 |
21
|
adantr |
⊢ ( ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) → ( 𝑐 × 𝑐 ) ≼ ω ) |
23 |
22
|
ad2antll |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( 𝑐 × 𝑐 ) ≼ ω ) |
24 |
|
domtr |
⊢ ( ( 𝑆 ≼ ( 𝑐 × 𝑐 ) ∧ ( 𝑐 × 𝑐 ) ≼ ω ) → 𝑆 ≼ ω ) |
25 |
13 23 24
|
sylancr |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → 𝑆 ≼ ω ) |
26 |
2
|
relopabiv |
⊢ Rel 𝑆 |
27 |
|
simpr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑆 ) |
28 |
|
1st2nd |
⊢ ( ( Rel 𝑆 ∧ 𝑥 ∈ 𝑆 ) → 𝑥 = 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ) |
29 |
26 27 28
|
sylancr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 = 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ) |
30 |
29 27
|
eqeltrrd |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ∈ 𝑆 ) |
31 |
|
df-br |
⊢ ( ( 1st ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑥 ) ↔ 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ∈ 𝑆 ) |
32 |
|
fvex |
⊢ ( 1st ‘ 𝑥 ) ∈ V |
33 |
|
fvex |
⊢ ( 2nd ‘ 𝑥 ) ∈ V |
34 |
|
simpl |
⊢ ( ( 𝑢 = ( 1st ‘ 𝑥 ) ∧ 𝑣 = ( 2nd ‘ 𝑥 ) ) → 𝑢 = ( 1st ‘ 𝑥 ) ) |
35 |
34
|
eleq1d |
⊢ ( ( 𝑢 = ( 1st ‘ 𝑥 ) ∧ 𝑣 = ( 2nd ‘ 𝑥 ) ) → ( 𝑢 ∈ 𝑐 ↔ ( 1st ‘ 𝑥 ) ∈ 𝑐 ) ) |
36 |
|
simpr |
⊢ ( ( 𝑢 = ( 1st ‘ 𝑥 ) ∧ 𝑣 = ( 2nd ‘ 𝑥 ) ) → 𝑣 = ( 2nd ‘ 𝑥 ) ) |
37 |
36
|
eleq1d |
⊢ ( ( 𝑢 = ( 1st ‘ 𝑥 ) ∧ 𝑣 = ( 2nd ‘ 𝑥 ) ) → ( 𝑣 ∈ 𝑐 ↔ ( 2nd ‘ 𝑥 ) ∈ 𝑐 ) ) |
38 |
|
sseq1 |
⊢ ( 𝑢 = ( 1st ‘ 𝑥 ) → ( 𝑢 ⊆ 𝑤 ↔ ( 1st ‘ 𝑥 ) ⊆ 𝑤 ) ) |
39 |
|
sseq2 |
⊢ ( 𝑣 = ( 2nd ‘ 𝑥 ) → ( 𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) |
40 |
38 39
|
bi2anan9 |
⊢ ( ( 𝑢 = ( 1st ‘ 𝑥 ) ∧ 𝑣 = ( 2nd ‘ 𝑥 ) ) → ( ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ↔ ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) ) |
41 |
40
|
rexbidv |
⊢ ( ( 𝑢 = ( 1st ‘ 𝑥 ) ∧ 𝑣 = ( 2nd ‘ 𝑥 ) ) → ( ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ↔ ∃ 𝑤 ∈ 𝐵 ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) ) |
42 |
35 37 41
|
3anbi123d |
⊢ ( ( 𝑢 = ( 1st ‘ 𝑥 ) ∧ 𝑣 = ( 2nd ‘ 𝑥 ) ) → ( ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ↔ ( ( 1st ‘ 𝑥 ) ∈ 𝑐 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) ) ) |
43 |
32 33 42 2
|
braba |
⊢ ( ( 1st ‘ 𝑥 ) 𝑆 ( 2nd ‘ 𝑥 ) ↔ ( ( 1st ‘ 𝑥 ) ∈ 𝑐 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) ) |
44 |
31 43
|
bitr3i |
⊢ ( 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ∈ 𝑆 ↔ ( ( 1st ‘ 𝑥 ) ∈ 𝑐 ∧ ( 2nd ‘ 𝑥 ) ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) ) |
45 |
44
|
simp3bi |
⊢ ( 〈 ( 1st ‘ 𝑥 ) , ( 2nd ‘ 𝑥 ) 〉 ∈ 𝑆 → ∃ 𝑤 ∈ 𝐵 ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) |
46 |
30 45
|
syl |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑤 ∈ 𝐵 ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) |
47 |
|
fvi |
⊢ ( 𝐵 ∈ TopBases → ( I ‘ 𝐵 ) = 𝐵 ) |
48 |
47
|
ad3antrrr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( I ‘ 𝐵 ) = 𝐵 ) |
49 |
48
|
rexeqdv |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ( ∃ 𝑤 ∈ ( I ‘ 𝐵 ) ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ↔ ∃ 𝑤 ∈ 𝐵 ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) ) |
50 |
46 49
|
mpbird |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → ∃ 𝑤 ∈ ( I ‘ 𝐵 ) ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) |
51 |
50
|
ralrimiva |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ∀ 𝑥 ∈ 𝑆 ∃ 𝑤 ∈ ( I ‘ 𝐵 ) ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) |
52 |
|
fvex |
⊢ ( I ‘ 𝐵 ) ∈ V |
53 |
|
sseq2 |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ↔ ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ) ) |
54 |
|
sseq1 |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ↔ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) |
55 |
53 54
|
anbi12d |
⊢ ( 𝑤 = ( 𝑓 ‘ 𝑥 ) → ( ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ↔ ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) |
56 |
52 55
|
axcc4dom |
⊢ ( ( 𝑆 ≼ ω ∧ ∀ 𝑥 ∈ 𝑆 ∃ 𝑤 ∈ ( I ‘ 𝐵 ) ( ( 1st ‘ 𝑥 ) ⊆ 𝑤 ∧ 𝑤 ⊆ ( 2nd ‘ 𝑥 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) |
57 |
25 51 56
|
syl2anc |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ∃ 𝑓 ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) |
58 |
47
|
ad2antrr |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( I ‘ 𝐵 ) = 𝐵 ) |
59 |
58
|
feq3d |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ↔ 𝑓 : 𝑆 ⟶ 𝐵 ) ) |
60 |
59
|
anbi1d |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ↔ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) ) |
61 |
|
2ndctop |
⊢ ( 𝐽 ∈ 2ndω → 𝐽 ∈ Top ) |
62 |
61
|
adantl |
⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) → 𝐽 ∈ Top ) |
63 |
62
|
ad2antrr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → 𝐽 ∈ Top ) |
64 |
|
frn |
⊢ ( 𝑓 : 𝑆 ⟶ 𝐵 → ran 𝑓 ⊆ 𝐵 ) |
65 |
64
|
ad2antrl |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ⊆ 𝐵 ) |
66 |
|
bastg |
⊢ ( 𝐵 ∈ TopBases → 𝐵 ⊆ ( topGen ‘ 𝐵 ) ) |
67 |
66
|
ad3antrrr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → 𝐵 ⊆ ( topGen ‘ 𝐵 ) ) |
68 |
67 1
|
sseqtrrdi |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → 𝐵 ⊆ 𝐽 ) |
69 |
65 68
|
sstrd |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ⊆ 𝐽 ) |
70 |
|
simprrl |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → 𝑜 ∈ 𝐽 ) |
71 |
|
simprr |
⊢ ( ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) → ( topGen ‘ 𝑐 ) = 𝐽 ) |
72 |
71
|
ad2antlr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → ( topGen ‘ 𝑐 ) = 𝐽 ) |
73 |
70 72
|
eleqtrrd |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → 𝑜 ∈ ( topGen ‘ 𝑐 ) ) |
74 |
|
simprrr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → 𝑡 ∈ 𝑜 ) |
75 |
|
tg2 |
⊢ ( ( 𝑜 ∈ ( topGen ‘ 𝑐 ) ∧ 𝑡 ∈ 𝑜 ) → ∃ 𝑑 ∈ 𝑐 ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) |
76 |
73 74 75
|
syl2anc |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → ∃ 𝑑 ∈ 𝑐 ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) |
77 |
|
bastg |
⊢ ( 𝑐 ∈ TopBases → 𝑐 ⊆ ( topGen ‘ 𝑐 ) ) |
78 |
77
|
ad2antrl |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → 𝑐 ⊆ ( topGen ‘ 𝑐 ) ) |
79 |
78
|
ad2antrr |
⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑐 ⊆ ( topGen ‘ 𝑐 ) ) |
80 |
1
|
eqeq2i |
⊢ ( ( topGen ‘ 𝑐 ) = 𝐽 ↔ ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) ) |
81 |
80
|
biimpi |
⊢ ( ( topGen ‘ 𝑐 ) = 𝐽 → ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) ) |
82 |
81
|
adantl |
⊢ ( ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) → ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) ) |
83 |
82
|
ad2antll |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) ) |
84 |
83
|
ad2antrr |
⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → ( topGen ‘ 𝑐 ) = ( topGen ‘ 𝐵 ) ) |
85 |
79 84
|
sseqtrd |
⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑐 ⊆ ( topGen ‘ 𝐵 ) ) |
86 |
|
simprl |
⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑑 ∈ 𝑐 ) |
87 |
85 86
|
sseldd |
⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑑 ∈ ( topGen ‘ 𝐵 ) ) |
88 |
|
simprrl |
⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑡 ∈ 𝑑 ) |
89 |
|
tg2 |
⊢ ( ( 𝑑 ∈ ( topGen ‘ 𝐵 ) ∧ 𝑡 ∈ 𝑑 ) → ∃ 𝑚 ∈ 𝐵 ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) |
90 |
87 88 89
|
syl2anc |
⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → ∃ 𝑚 ∈ 𝐵 ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) |
91 |
66
|
ad3antrrr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → 𝐵 ⊆ ( topGen ‘ 𝐵 ) ) |
92 |
91
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝐵 ⊆ ( topGen ‘ 𝐵 ) ) |
93 |
72
|
ad2antrr |
⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → ( topGen ‘ 𝑐 ) = 𝐽 ) |
94 |
93 1
|
eqtr2di |
⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → ( topGen ‘ 𝐵 ) = ( topGen ‘ 𝑐 ) ) |
95 |
92 94
|
sseqtrd |
⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝐵 ⊆ ( topGen ‘ 𝑐 ) ) |
96 |
|
simprl |
⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝑚 ∈ 𝐵 ) |
97 |
95 96
|
sseldd |
⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝑚 ∈ ( topGen ‘ 𝑐 ) ) |
98 |
|
simprrl |
⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝑡 ∈ 𝑚 ) |
99 |
|
tg2 |
⊢ ( ( 𝑚 ∈ ( topGen ‘ 𝑐 ) ∧ 𝑡 ∈ 𝑚 ) → ∃ 𝑛 ∈ 𝑐 ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) |
100 |
97 98 99
|
syl2anc |
⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → ∃ 𝑛 ∈ 𝑐 ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) |
101 |
|
ffn |
⊢ ( 𝑓 : 𝑆 ⟶ 𝐵 → 𝑓 Fn 𝑆 ) |
102 |
101
|
ad2antrr |
⊢ ( ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) → 𝑓 Fn 𝑆 ) |
103 |
102
|
ad2antlr |
⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → 𝑓 Fn 𝑆 ) |
104 |
103
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑓 Fn 𝑆 ) |
105 |
|
simprl |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑛 ∈ 𝑐 ) |
106 |
86
|
ad2antrr |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑑 ∈ 𝑐 ) |
107 |
|
simplrl |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑚 ∈ 𝐵 ) |
108 |
|
simprrr |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑛 ⊆ 𝑚 ) |
109 |
|
simprr |
⊢ ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → 𝑚 ⊆ 𝑑 ) |
110 |
109
|
ad2antlr |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑚 ⊆ 𝑑 ) |
111 |
|
sseq2 |
⊢ ( 𝑤 = 𝑚 → ( 𝑛 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑚 ) ) |
112 |
|
sseq1 |
⊢ ( 𝑤 = 𝑚 → ( 𝑤 ⊆ 𝑑 ↔ 𝑚 ⊆ 𝑑 ) ) |
113 |
111 112
|
anbi12d |
⊢ ( 𝑤 = 𝑚 → ( ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ↔ ( 𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) |
114 |
113
|
rspcev |
⊢ ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑛 ⊆ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) |
115 |
107 108 110 114
|
syl12anc |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) |
116 |
|
df-br |
⊢ ( 𝑛 𝑆 𝑑 ↔ 〈 𝑛 , 𝑑 〉 ∈ 𝑆 ) |
117 |
|
vex |
⊢ 𝑛 ∈ V |
118 |
|
vex |
⊢ 𝑑 ∈ V |
119 |
|
simpl |
⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → 𝑢 = 𝑛 ) |
120 |
119
|
eleq1d |
⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( 𝑢 ∈ 𝑐 ↔ 𝑛 ∈ 𝑐 ) ) |
121 |
|
simpr |
⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → 𝑣 = 𝑑 ) |
122 |
121
|
eleq1d |
⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( 𝑣 ∈ 𝑐 ↔ 𝑑 ∈ 𝑐 ) ) |
123 |
|
sseq1 |
⊢ ( 𝑢 = 𝑛 → ( 𝑢 ⊆ 𝑤 ↔ 𝑛 ⊆ 𝑤 ) ) |
124 |
|
sseq2 |
⊢ ( 𝑣 = 𝑑 → ( 𝑤 ⊆ 𝑣 ↔ 𝑤 ⊆ 𝑑 ) ) |
125 |
123 124
|
bi2anan9 |
⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ↔ ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) ) |
126 |
125
|
rexbidv |
⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ↔ ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) ) |
127 |
120 122 126
|
3anbi123d |
⊢ ( ( 𝑢 = 𝑛 ∧ 𝑣 = 𝑑 ) → ( ( 𝑢 ∈ 𝑐 ∧ 𝑣 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑢 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑣 ) ) ↔ ( 𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) ) ) |
128 |
117 118 127 2
|
braba |
⊢ ( 𝑛 𝑆 𝑑 ↔ ( 𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) ) |
129 |
116 128
|
bitr3i |
⊢ ( 〈 𝑛 , 𝑑 〉 ∈ 𝑆 ↔ ( 𝑛 ∈ 𝑐 ∧ 𝑑 ∈ 𝑐 ∧ ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) ) |
130 |
105 106 115 129
|
syl3anbrc |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 〈 𝑛 , 𝑑 〉 ∈ 𝑆 ) |
131 |
|
fnfvelrn |
⊢ ( ( 𝑓 Fn 𝑆 ∧ 〈 𝑛 , 𝑑 〉 ∈ 𝑆 ) → ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∈ ran 𝑓 ) |
132 |
104 130 131
|
syl2anc |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∈ ran 𝑓 ) |
133 |
|
simprl |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑛 ∈ 𝑐 ) |
134 |
|
simplll |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑑 ∈ 𝑐 ) |
135 |
|
simplrl |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑚 ∈ 𝐵 ) |
136 |
|
simprrr |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑛 ⊆ 𝑚 ) |
137 |
109
|
ad2antlr |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 𝑚 ⊆ 𝑑 ) |
138 |
135 136 137 114
|
syl12anc |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ∃ 𝑤 ∈ 𝐵 ( 𝑛 ⊆ 𝑤 ∧ 𝑤 ⊆ 𝑑 ) ) |
139 |
133 134 138 129
|
syl3anbrc |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → 〈 𝑛 , 𝑑 〉 ∈ 𝑆 ) |
140 |
|
fveq2 |
⊢ ( 𝑥 = 〈 𝑛 , 𝑑 〉 → ( 1st ‘ 𝑥 ) = ( 1st ‘ 〈 𝑛 , 𝑑 〉 ) ) |
141 |
|
fveq2 |
⊢ ( 𝑥 = 〈 𝑛 , 𝑑 〉 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ) |
142 |
140 141
|
sseq12d |
⊢ ( 𝑥 = 〈 𝑛 , 𝑑 〉 → ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ↔ ( 1st ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ) ) |
143 |
|
fveq2 |
⊢ ( 𝑥 = 〈 𝑛 , 𝑑 〉 → ( 2nd ‘ 𝑥 ) = ( 2nd ‘ 〈 𝑛 , 𝑑 〉 ) ) |
144 |
141 143
|
sseq12d |
⊢ ( 𝑥 = 〈 𝑛 , 𝑑 〉 → ( ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ↔ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 2nd ‘ 〈 𝑛 , 𝑑 〉 ) ) ) |
145 |
142 144
|
anbi12d |
⊢ ( 𝑥 = 〈 𝑛 , 𝑑 〉 → ( ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ↔ ( ( 1st ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 2nd ‘ 〈 𝑛 , 𝑑 〉 ) ) ) ) |
146 |
145
|
rspcv |
⊢ ( 〈 𝑛 , 𝑑 〉 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) → ( ( 1st ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 2nd ‘ 〈 𝑛 , 𝑑 〉 ) ) ) ) |
147 |
139 146
|
syl |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) → ( ( 1st ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 2nd ‘ 〈 𝑛 , 𝑑 〉 ) ) ) ) |
148 |
117 118
|
op1st |
⊢ ( 1st ‘ 〈 𝑛 , 𝑑 〉 ) = 𝑛 |
149 |
148
|
sseq1i |
⊢ ( ( 1st ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ↔ 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ) |
150 |
117 118
|
op2nd |
⊢ ( 2nd ‘ 〈 𝑛 , 𝑑 〉 ) = 𝑑 |
151 |
150
|
sseq2i |
⊢ ( ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 2nd ‘ 〈 𝑛 , 𝑑 〉 ) ↔ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) |
152 |
149 151
|
anbi12i |
⊢ ( ( ( 1st ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 2nd ‘ 〈 𝑛 , 𝑑 〉 ) ) ↔ ( 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) ) |
153 |
|
simprl |
⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) ) → 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ) |
154 |
|
simprl |
⊢ ( ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) → 𝑡 ∈ 𝑛 ) |
155 |
154
|
ad2antlr |
⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) ) → 𝑡 ∈ 𝑛 ) |
156 |
153 155
|
sseldd |
⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) ) → 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ) |
157 |
|
simprr |
⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) ) → ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) |
158 |
|
simplrr |
⊢ ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → 𝑑 ⊆ 𝑜 ) |
159 |
158
|
ad2antrr |
⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) ) → 𝑑 ⊆ 𝑜 ) |
160 |
157 159
|
sstrd |
⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) ) → ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) |
161 |
156 160
|
jca |
⊢ ( ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) ∧ ( 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) ) → ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) |
162 |
161
|
ex |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( ( 𝑛 ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑑 ) → ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) ) |
163 |
152 162
|
syl5bi |
⊢ ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( ( ( 1st ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ ( 2nd ‘ 〈 𝑛 , 𝑑 〉 ) ) → ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) ) |
164 |
147 163
|
syldc |
⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) → ( ( ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) ) |
165 |
164
|
exp4c |
⊢ ( ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) → ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) → ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → ( ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) → ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) ) ) ) |
166 |
165
|
ad2antlr |
⊢ ( ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) → ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) → ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → ( ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) → ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) ) ) ) |
167 |
166
|
adantl |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → ( ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) → ( ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) → ( ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) → ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) ) ) ) |
168 |
167
|
imp41 |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) |
169 |
|
eleq2 |
⊢ ( 𝑏 = ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) → ( 𝑡 ∈ 𝑏 ↔ 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ) ) |
170 |
|
sseq1 |
⊢ ( 𝑏 = ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) → ( 𝑏 ⊆ 𝑜 ↔ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) |
171 |
169 170
|
anbi12d |
⊢ ( 𝑏 = ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) → ( ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ↔ ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) ) |
172 |
171
|
rspcev |
⊢ ( ( ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∈ ran 𝑓 ∧ ( 𝑡 ∈ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ∧ ( 𝑓 ‘ 〈 𝑛 , 𝑑 〉 ) ⊆ 𝑜 ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) |
173 |
132 168 172
|
syl2anc |
⊢ ( ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) ∧ ( 𝑛 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑛 ∧ 𝑛 ⊆ 𝑚 ) ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) |
174 |
100 173
|
rexlimddv |
⊢ ( ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) ∧ ( 𝑚 ∈ 𝐵 ∧ ( 𝑡 ∈ 𝑚 ∧ 𝑚 ⊆ 𝑑 ) ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) |
175 |
90 174
|
rexlimddv |
⊢ ( ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) ∧ ( 𝑑 ∈ 𝑐 ∧ ( 𝑡 ∈ 𝑑 ∧ 𝑑 ⊆ 𝑜 ) ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) |
176 |
76 175
|
rexlimddv |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ∧ ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) ) ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) |
177 |
176
|
expr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ( ( 𝑜 ∈ 𝐽 ∧ 𝑡 ∈ 𝑜 ) → ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) ) |
178 |
177
|
ralrimivv |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ∀ 𝑜 ∈ 𝐽 ∀ 𝑡 ∈ 𝑜 ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) |
179 |
|
basgen2 |
⊢ ( ( 𝐽 ∈ Top ∧ ran 𝑓 ⊆ 𝐽 ∧ ∀ 𝑜 ∈ 𝐽 ∀ 𝑡 ∈ 𝑜 ∃ 𝑏 ∈ ran 𝑓 ( 𝑡 ∈ 𝑏 ∧ 𝑏 ⊆ 𝑜 ) ) → ( topGen ‘ ran 𝑓 ) = 𝐽 ) |
180 |
63 69 178 179
|
syl3anc |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ( topGen ‘ ran 𝑓 ) = 𝐽 ) |
181 |
180 63
|
eqeltrd |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ( topGen ‘ ran 𝑓 ) ∈ Top ) |
182 |
|
tgclb |
⊢ ( ran 𝑓 ∈ TopBases ↔ ( topGen ‘ ran 𝑓 ) ∈ Top ) |
183 |
181 182
|
sylibr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ∈ TopBases ) |
184 |
|
omelon |
⊢ ω ∈ On |
185 |
25
|
adantr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → 𝑆 ≼ ω ) |
186 |
|
ondomen |
⊢ ( ( ω ∈ On ∧ 𝑆 ≼ ω ) → 𝑆 ∈ dom card ) |
187 |
184 185 186
|
sylancr |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → 𝑆 ∈ dom card ) |
188 |
101
|
ad2antrl |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → 𝑓 Fn 𝑆 ) |
189 |
|
dffn4 |
⊢ ( 𝑓 Fn 𝑆 ↔ 𝑓 : 𝑆 –onto→ ran 𝑓 ) |
190 |
188 189
|
sylib |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → 𝑓 : 𝑆 –onto→ ran 𝑓 ) |
191 |
|
fodomnum |
⊢ ( 𝑆 ∈ dom card → ( 𝑓 : 𝑆 –onto→ ran 𝑓 → ran 𝑓 ≼ 𝑆 ) ) |
192 |
187 190 191
|
sylc |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ≼ 𝑆 ) |
193 |
|
domtr |
⊢ ( ( ran 𝑓 ≼ 𝑆 ∧ 𝑆 ≼ ω ) → ran 𝑓 ≼ ω ) |
194 |
192 185 193
|
syl2anc |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ran 𝑓 ≼ ω ) |
195 |
180
|
eqcomd |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → 𝐽 = ( topGen ‘ ran 𝑓 ) ) |
196 |
|
breq1 |
⊢ ( 𝑏 = ran 𝑓 → ( 𝑏 ≼ ω ↔ ran 𝑓 ≼ ω ) ) |
197 |
|
sseq1 |
⊢ ( 𝑏 = ran 𝑓 → ( 𝑏 ⊆ 𝐵 ↔ ran 𝑓 ⊆ 𝐵 ) ) |
198 |
|
fveq2 |
⊢ ( 𝑏 = ran 𝑓 → ( topGen ‘ 𝑏 ) = ( topGen ‘ ran 𝑓 ) ) |
199 |
198
|
eqeq2d |
⊢ ( 𝑏 = ran 𝑓 → ( 𝐽 = ( topGen ‘ 𝑏 ) ↔ 𝐽 = ( topGen ‘ ran 𝑓 ) ) ) |
200 |
196 197 199
|
3anbi123d |
⊢ ( 𝑏 = ran 𝑓 → ( ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ↔ ( ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ ran 𝑓 ) ) ) ) |
201 |
200
|
rspcev |
⊢ ( ( ran 𝑓 ∈ TopBases ∧ ( ran 𝑓 ≼ ω ∧ ran 𝑓 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ ran 𝑓 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) |
202 |
183 194 65 195 201
|
syl13anc |
⊢ ( ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) ∧ ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) |
203 |
202
|
ex |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( ( 𝑓 : 𝑆 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) ) |
204 |
60 203
|
sylbid |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) ) |
205 |
204
|
exlimdv |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑆 ⟶ ( I ‘ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝑆 ( ( 1st ‘ 𝑥 ) ⊆ ( 𝑓 ‘ 𝑥 ) ∧ ( 𝑓 ‘ 𝑥 ) ⊆ ( 2nd ‘ 𝑥 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) ) |
206 |
57 205
|
mpd |
⊢ ( ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) ∧ ( 𝑐 ∈ TopBases ∧ ( 𝑐 ≼ ω ∧ ( topGen ‘ 𝑐 ) = 𝐽 ) ) ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) |
207 |
5 206
|
rexlimddv |
⊢ ( ( 𝐵 ∈ TopBases ∧ 𝐽 ∈ 2ndω ) → ∃ 𝑏 ∈ TopBases ( 𝑏 ≼ ω ∧ 𝑏 ⊆ 𝐵 ∧ 𝐽 = ( topGen ‘ 𝑏 ) ) ) |