Step |
Hyp |
Ref |
Expression |
1 |
|
df-ufil |
⊢ UFil = ( 𝑦 ∈ V ↦ { 𝑧 ∈ ( Fil ‘ 𝑦 ) ∣ ∀ 𝑥 ∈ 𝒫 𝑦 ( 𝑥 ∈ 𝑧 ∨ ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ) } ) |
2 |
|
pweq |
⊢ ( 𝑦 = 𝑋 → 𝒫 𝑦 = 𝒫 𝑋 ) |
3 |
2
|
adantr |
⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → 𝒫 𝑦 = 𝒫 𝑋 ) |
4 |
|
eleq2 |
⊢ ( 𝑧 = 𝐹 → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐹 ) ) |
5 |
4
|
adantl |
⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → ( 𝑥 ∈ 𝑧 ↔ 𝑥 ∈ 𝐹 ) ) |
6 |
|
difeq1 |
⊢ ( 𝑦 = 𝑋 → ( 𝑦 ∖ 𝑥 ) = ( 𝑋 ∖ 𝑥 ) ) |
7 |
|
eleq12 |
⊢ ( ( ( 𝑦 ∖ 𝑥 ) = ( 𝑋 ∖ 𝑥 ) ∧ 𝑧 = 𝐹 ) → ( ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
8 |
6 7
|
sylan |
⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → ( ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ↔ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) |
9 |
5 8
|
orbi12d |
⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → ( ( 𝑥 ∈ 𝑧 ∨ ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ) ↔ ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) ) |
10 |
3 9
|
raleqbidv |
⊢ ( ( 𝑦 = 𝑋 ∧ 𝑧 = 𝐹 ) → ( ∀ 𝑥 ∈ 𝒫 𝑦 ( 𝑥 ∈ 𝑧 ∨ ( 𝑦 ∖ 𝑥 ) ∈ 𝑧 ) ↔ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) ) |
11 |
|
fveq2 |
⊢ ( 𝑦 = 𝑋 → ( Fil ‘ 𝑦 ) = ( Fil ‘ 𝑋 ) ) |
12 |
|
fvex |
⊢ ( Fil ‘ 𝑦 ) ∈ V |
13 |
|
elfvdm |
⊢ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) → 𝑋 ∈ dom Fil ) |
14 |
1 10 11 12 13
|
elmptrab2 |
⊢ ( 𝐹 ∈ ( UFil ‘ 𝑋 ) ↔ ( 𝐹 ∈ ( Fil ‘ 𝑋 ) ∧ ∀ 𝑥 ∈ 𝒫 𝑋 ( 𝑥 ∈ 𝐹 ∨ ( 𝑋 ∖ 𝑥 ) ∈ 𝐹 ) ) ) |