Step |
Hyp |
Ref |
Expression |
1 |
|
elrnust |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑈 ∈ ∪ ran UnifOn ) |
2 |
|
unieq |
⊢ ( 𝑢 = 𝑈 → ∪ 𝑢 = ∪ 𝑈 ) |
3 |
2
|
dmeqd |
⊢ ( 𝑢 = 𝑈 → dom ∪ 𝑢 = dom ∪ 𝑈 ) |
4 |
3
|
fveq2d |
⊢ ( 𝑢 = 𝑈 → ( fBas ‘ dom ∪ 𝑢 ) = ( fBas ‘ dom ∪ 𝑈 ) ) |
5 |
|
raleq |
⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) |
6 |
4 5
|
rabeqbidv |
⊢ ( 𝑢 = 𝑈 → { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } = { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ) |
7 |
|
df-cfilu |
⊢ CauFilu = ( 𝑢 ∈ ∪ ran UnifOn ↦ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑢 ) ∣ ∀ 𝑣 ∈ 𝑢 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ) |
8 |
|
fvex |
⊢ ( fBas ‘ dom ∪ 𝑈 ) ∈ V |
9 |
8
|
rabex |
⊢ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ∈ V |
10 |
6 7 9
|
fvmpt |
⊢ ( 𝑈 ∈ ∪ ran UnifOn → ( CauFilu ‘ 𝑈 ) = { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ) |
11 |
1 10
|
syl |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( CauFilu ‘ 𝑈 ) = { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ) |
12 |
11
|
eleq2d |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ 𝐹 ∈ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ) ) |
13 |
|
rexeq |
⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) |
14 |
13
|
ralbidv |
⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ↔ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) |
15 |
14
|
elrab |
⊢ ( 𝐹 ∈ { 𝑓 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∣ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝑓 ( 𝑎 × 𝑎 ) ⊆ 𝑣 } ↔ ( 𝐹 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) |
16 |
12 15
|
bitrdi |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) ) |
17 |
|
ustbas2 |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → 𝑋 = dom ∪ 𝑈 ) |
18 |
17
|
fveq2d |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( fBas ‘ 𝑋 ) = ( fBas ‘ dom ∪ 𝑈 ) ) |
19 |
18
|
eleq2d |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ↔ 𝐹 ∈ ( fBas ‘ dom ∪ 𝑈 ) ) ) |
20 |
19
|
anbi1d |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ↔ ( 𝐹 ∈ ( fBas ‘ dom ∪ 𝑈 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) ) |
21 |
16 20
|
bitr4d |
⊢ ( 𝑈 ∈ ( UnifOn ‘ 𝑋 ) → ( 𝐹 ∈ ( CauFilu ‘ 𝑈 ) ↔ ( 𝐹 ∈ ( fBas ‘ 𝑋 ) ∧ ∀ 𝑣 ∈ 𝑈 ∃ 𝑎 ∈ 𝐹 ( 𝑎 × 𝑎 ) ⊆ 𝑣 ) ) ) |