Metamath Proof Explorer

Theorem mnuop3d

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

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

Proof

Step Hyp Ref Expression
1 mnuop3d.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 mnuop3d.2 ⊢ φ → U ∈ M
3 mnuop3d.3 ⊢ φ → A ∈ U
4 mnuop3d.4 ⊢ φ → F ⊆ U
5 2 4 sselpwd ⊢ φ → F ∈ 𝒫 U
6 1 2 3 5 mnuop23d ⊢ φ → ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
7 4 sseld ⊢ φ → v ∈ F → v ∈ U
8 7 adantrd ⊢ φ → v ∈ F ∧ i ∈ v → v ∈ U
9 pm3.22 ⊢ v ∈ F ∧ i ∈ v → i ∈ v ∧ v ∈ F
10 8 9 jca2 ⊢ φ → v ∈ F ∧ i ∈ v → v ∈ U ∧ i ∈ v ∧ v ∈ F
11 10 reximdv2 ⊢ φ → ∃ v ∈ F i ∈ v → ∃ v ∈ U i ∈ v ∧ v ∈ F
12 11 imim1d ⊢ φ → ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
13 12 ralimdv ⊢ φ → ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ∀ i ∈ A ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
14 13 adantld ⊢ φ → 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ∀ i ∈ A ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
15 14 reximdv ⊢ φ → ∃ w ∈ U 𝒫 A ⊆ w ∧ ∀ i ∈ A ∃ v ∈ U i ∈ v ∧ v ∈ F → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ∃ w ∈ U ∀ i ∈ A ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
16 6 15 mpd ⊢ φ → ∃ w ∈ U ∀ i ∈ A ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w