Metamath Proof Explorer

Theorem mnuop23d

Description: Second and third operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuop23d.1 ⊢ M = k | ∀ l ∈ k 𝒫 l ⊆ k ∧ ∀ m ∃ n ∈ k 𝒫 l ⊆ n ∧ ∀ p ∈ l ∃ q ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ r ∧ ⋃ r ⊆ n
mnuop23d.2 ⊢ φ → U ∈ M
mnuop23d.3 ⊢ φ → A ∈ U
mnuop23d.4 ⊢ φ → F ∈ V
Assertion mnuop23d ⊢ φ → ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w

Proof

Step Hyp Ref Expression
1 mnuop23d.1 ⊢ M = k | ∀ l ∈ k 𝒫 l ⊆ k ∧ ∀ m ∃ n ∈ k 𝒫 l ⊆ n ∧ ∀ p ∈ l ∃ q ∈ k p ∈ q ∧ q ∈ m → ∃ r ∈ m p ∈ r ∧ ⋃ r ⊆ n
2 mnuop23d.2 ⊢ φ → U ∈ M
3 mnuop23d.3 ⊢ φ → A ∈ U
4 mnuop23d.4 ⊢ φ → F ∈ V
5 1 2 3 mnuop123d ⊢ φ → 𝒫 A ⊆ U ∧ ∀ f ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
6 5 simprd ⊢ φ → ∀ f ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
7 eleq2 ⊢ f = F → v ∈ f ↔ v ∈ F
8 7 anbi2d ⊢ f = F → i ∈ v ∧ v ∈ f ↔ i ∈ v ∧ v ∈ F
9 8 rexbidv ⊢ f = F → ∃ v ∈ U i ∈ v ∧ v ∈ f ↔ ∃ v ∈ U i ∈ v ∧ v ∈ F
10 rexeq ⊢ f = F → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w ↔ ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
11 9 10 imbi12d ⊢ f = F → ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w ↔ ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
12 11 ralbidv ⊢ f = F → ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w ↔ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
13 12 anbi2d ⊢ f = F → 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w ↔ 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
14 13 rexbidv ⊢ f = F → ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w ↔ ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
15 14 spcgv ⊢ F ∈ V → ∀ f ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w → ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
16 4 6 15 sylc ⊢ φ → ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w