Metamath Proof Explorer

Theorem mnuprdlem4

Description: Lemma for mnuprd . General case. (Contributed by Rohan Ridenour, 13-Aug-2023)

Ref Expression
Hypotheses mnuprdlem4.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
mnuprdlem4.2 ⊢ F = ∅ A ∅ B
mnuprdlem4.3 ⊢ φ → U ∈ M
mnuprdlem4.4 ⊢ φ → A ∈ U
mnuprdlem4.5 ⊢ φ → B ∈ U
mnuprdlem4.6 ⊢ φ → ¬ A = ∅
Assertion mnuprdlem4 ⊢ φ → A B ∈ U

Proof

Step Hyp Ref Expression
1 mnuprdlem4.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 mnuprdlem4.2 ⊢ F = ∅ A ∅ B
3 mnuprdlem4.3 ⊢ φ → U ∈ M
4 mnuprdlem4.4 ⊢ φ → A ∈ U
5 mnuprdlem4.5 ⊢ φ → B ∈ U
6 mnuprdlem4.6 ⊢ φ → ¬ A = ∅
7 1 3 4 mnu0eld ⊢ φ → ∅ ∈ U
8 1 3 7 mnusnd ⊢ φ → ∅ ∈ U
9 0ss ⊢ ∅ ⊆ ∅
10 ssid ⊢ ∅ ⊆ ∅
11 1 3 8 9 10 mnuprss2d ⊢ φ → ∅ ∅ ∈ U
12 1 3 4 mnusnd ⊢ φ → A ∈ U
13 0ss ⊢ ∅ ⊆ A
14 ssid ⊢ A ⊆ A
15 1 3 12 13 14 mnuprss2d ⊢ φ → ∅ A ∈ U
16 0ss ⊢ ∅ ⊆ B
17 ssid ⊢ B ⊆ B
18 1 3 5 16 17 mnuprss2d ⊢ φ → ∅ B ∈ U
19 snsspr1 ⊢ ∅ ⊆ ∅ B
20 snsspr2 ⊢ B ⊆ ∅ B
21 1 3 18 19 20 mnuprss2d ⊢ φ → ∅ B ∈ U
22 15 21 prssd ⊢ φ → ∅ A ∅ B ⊆ U
23 2 22 eqsstrid ⊢ φ → F ⊆ U
24 1 3 11 23 mnuop3d ⊢ φ → ∃ w ∈ U ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
25 simprl ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → w ∈ U
26 eleq2w ⊢ a = w → A ∈ a ↔ A ∈ w
27 eleq2w ⊢ a = w → B ∈ a ↔ B ∈ w
28 26 27 anbi12d ⊢ a = w → A ∈ a ∧ B ∈ a ↔ A ∈ w ∧ B ∈ w
29 28 adantl ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w ∧ a = w → A ∈ a ∧ B ∈ a ↔ A ∈ w ∧ B ∈ w
30 4 adantr ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → A ∈ U
31 5 adantr ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → B ∈ U
32 nfv ⊢ Ⅎ i φ
33 nfv ⊢ Ⅎ i w ∈ U
34 nfra1 ⊢ Ⅎ i ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
35 33 34 nfan ⊢ Ⅎ i w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
36 32 35 nfan ⊢ Ⅎ i φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
37 2 36 mnuprdlem3 ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v
38 ralim ⊢ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∀ i ∈ ∅ ∅ ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
39 38 ad2antll ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∀ i ∈ ∅ ∅ ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
40 37 39 mpd ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ∀ i ∈ ∅ ∅ ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
41 2 30 31 40 mnuprdlem1 ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → A ∈ w
42 6 adantr ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ¬ A = ∅
43 2 31 42 40 mnuprdlem2 ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → B ∈ w
44 41 43 jca ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → A ∈ w ∧ B ∈ w
45 25 29 44 rspcedvd ⊢ φ ∧ w ∈ U ∧ ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w → ∃ a ∈ U A ∈ a ∧ B ∈ a
46 24 45 rexlimddv ⊢ φ → ∃ a ∈ U A ∈ a ∧ B ∈ a
47 3 adantr ⊢ φ ∧ a ∈ U ∧ A ∈ a ∧ B ∈ a → U ∈ M
48 simprl ⊢ φ ∧ a ∈ U ∧ A ∈ a ∧ B ∈ a → a ∈ U
49 simprrl ⊢ φ ∧ a ∈ U ∧ A ∈ a ∧ B ∈ a → A ∈ a
50 simprrr ⊢ φ ∧ a ∈ U ∧ A ∈ a ∧ B ∈ a → B ∈ a
51 49 50 prssd ⊢ φ ∧ a ∈ U ∧ A ∈ a ∧ B ∈ a → A B ⊆ a
52 1 47 48 51 mnussd ⊢ φ ∧ a ∈ U ∧ A ∈ a ∧ B ∈ a → A B ∈ U
53 46 52 rexlimddv ⊢ φ → A B ∈ U