Step |
Hyp |
Ref |
Expression |
1 |
|
mnuop23d.1 |
⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) } |
2 |
|
mnuop23d.2 |
⊢ ( 𝜑 → 𝑈 ∈ 𝑀 ) |
3 |
|
mnuop23d.3 |
⊢ ( 𝜑 → 𝐴 ∈ 𝑈 ) |
4 |
|
mnuop23d.4 |
⊢ ( 𝜑 → 𝐹 ∈ 𝑉 ) |
5 |
1 2 3
|
mnuop123d |
⊢ ( 𝜑 → ( 𝒫 𝐴 ⊆ 𝑈 ∧ ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
6 |
5
|
simprd |
⊢ ( 𝜑 → ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) |
7 |
|
eleq2 |
⊢ ( 𝑓 = 𝐹 → ( 𝑣 ∈ 𝑓 ↔ 𝑣 ∈ 𝐹 ) ) |
8 |
7
|
anbi2d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ↔ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) ) ) |
9 |
8
|
rexbidv |
⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) ↔ ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) ) ) |
10 |
|
rexeq |
⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) |
11 |
9 10
|
imbi12d |
⊢ ( 𝑓 = 𝐹 → ( ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) |
12 |
11
|
ralbidv |
⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ↔ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) |
13 |
12
|
anbi2d |
⊢ ( 𝑓 = 𝐹 → ( ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ↔ ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
14 |
13
|
rexbidv |
⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ↔ ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
15 |
14
|
spcgv |
⊢ ( 𝐹 ∈ 𝑉 → ( ∀ 𝑓 ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝑓 ) → ∃ 𝑢 ∈ 𝑓 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ) |
16 |
4 6 15
|
sylc |
⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) |