Metamath Proof Explorer

Theorem mnuop123d

Description: Operations of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuop123d.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
mnuop123d.2 ⊢ φ → U ∈ M
mnuop123d.3 ⊢ φ → A ∈ U
Assertion mnuop123d ⊢ φ → 𝒫 A ⊆ U ∧ ∀ f ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w

Proof

Step Hyp Ref Expression
1 mnuop123d.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 mnuop123d.2 ⊢ φ → U ∈ M
3 mnuop123d.3 ⊢ φ → A ∈ U
4 pweq ⊢ z = A → 𝒫 z = 𝒫 A
5 4 sseq1d ⊢ z = A → 𝒫 z ⊆ U ↔ 𝒫 A ⊆ U
6 4 sseq1d ⊢ z = A → 𝒫 z ⊆ w ↔ 𝒫 A ⊆ w
7 raleq ⊢ z = A → ∀ i ∈ z ∃ 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
8 6 7 anbi12d ⊢ z = A → 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ 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
9 8 rexbidv ⊢ z = A → ∃ w ∈ U 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ 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
10 9 albidv ⊢ z = A → ∀ f ∃ w ∈ U 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w ↔ ∀ f ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
11 5 10 anbi12d ⊢ z = A → 𝒫 z ⊆ U ∧ ∀ f ∃ w ∈ U 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w ↔ 𝒫 A ⊆ U ∧ ∀ f ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
12 1 ismnu ⊢ U ∈ M → U ∈ M ↔ ∀ z ∈ U 𝒫 z ⊆ U ∧ ∀ f ∃ w ∈ U 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
13 12 ibi ⊢ U ∈ M → ∀ z ∈ U 𝒫 z ⊆ U ∧ ∀ f ∃ w ∈ U 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
14 2 13 syl ⊢ φ → ∀ z ∈ U 𝒫 z ⊆ U ∧ ∀ f ∃ w ∈ U 𝒫 z ⊆ w ∧ ∀ i ∈ z ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w
15 11 14 3 rspcdva ⊢ φ → 𝒫 A ⊆ U ∧ ∀ f ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ f → ∃ u ∈ f i ∈ u ∧ ⋃ u ⊆ w