Step |
Hyp |
Ref |
Expression |
1 |
|
ordttopon.3 |
⊢ 𝑋 = dom 𝑅 |
2 |
|
eqid |
⊢ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) |
3 |
|
eqid |
⊢ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) |
4 |
1 2 3
|
ordtuni |
⊢ ( 𝑅 ∈ 𝑉 → 𝑋 = ∪ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) |
5 |
4
|
adantr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → 𝑋 = ∪ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) |
6 |
|
dmexg |
⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V ) |
7 |
1 6
|
eqeltrid |
⊢ ( 𝑅 ∈ 𝑉 → 𝑋 ∈ V ) |
8 |
7
|
adantr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → 𝑋 ∈ V ) |
9 |
5 8
|
eqeltrrd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ∪ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V ) |
10 |
|
uniexb |
⊢ ( ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V ↔ ∪ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V ) |
11 |
9 10
|
sylibr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V ) |
12 |
|
ssfii |
⊢ ( ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) |
13 |
11 12
|
syl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) |
14 |
|
fibas |
⊢ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ∈ TopBases |
15 |
|
bastg |
⊢ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ∈ TopBases → ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) ) |
16 |
14 15
|
ax-mp |
⊢ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) |
17 |
13 16
|
sstrdi |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) ) |
18 |
1 2 3
|
ordtval |
⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) ) |
19 |
18
|
adantr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) ) |
20 |
17 19
|
sseqtrrd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( ordTop ‘ 𝑅 ) ) |
21 |
|
ssun2 |
⊢ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ⊆ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) |
22 |
|
ssun1 |
⊢ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ⊆ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) |
23 |
|
simpr |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 ) |
24 |
|
eqidd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ) |
25 |
|
breq2 |
⊢ ( 𝑦 = 𝑃 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝑃 ) ) |
26 |
25
|
notbid |
⊢ ( 𝑦 = 𝑃 → ( ¬ 𝑥 𝑅 𝑦 ↔ ¬ 𝑥 𝑅 𝑃 ) ) |
27 |
26
|
rabbidv |
⊢ ( 𝑦 = 𝑃 → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ) |
28 |
27
|
rspceeqv |
⊢ ( ( 𝑃 ∈ 𝑋 ∧ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ) → ∃ 𝑦 ∈ 𝑋 { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) |
29 |
23 24 28
|
syl2anc |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) |
30 |
|
rabexg |
⊢ ( 𝑋 ∈ V → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ V ) |
31 |
|
eqid |
⊢ ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) |
32 |
31
|
elrnmpt |
⊢ ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ V → ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ↔ ∃ 𝑦 ∈ 𝑋 { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) |
33 |
8 30 32
|
3syl |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ↔ ∃ 𝑦 ∈ 𝑋 { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) |
34 |
29 33
|
mpbird |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) |
35 |
22 34
|
sselid |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) |
36 |
21 35
|
sselid |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) |
37 |
20 36
|
sseldd |
⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑃 } ∈ ( ordTop ‘ 𝑅 ) ) |