Metamath Proof Explorer

Theorem mnuprdlem2

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

Ref Expression
Hypotheses mnuprdlem2.1 ⊢ F = ∅ A ∅ B
mnuprdlem2.4 ⊢ φ → B ∈ U
mnuprdlem2.5 ⊢ φ → ¬ A = ∅
mnuprdlem2.8 ⊢ φ → ∀ i ∈ ∅ ∅ ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
Assertion mnuprdlem2 ⊢ φ → B ∈ w

Proof

Step Hyp Ref Expression
1 mnuprdlem2.1 ⊢ F = ∅ A ∅ B
2 mnuprdlem2.4 ⊢ φ → B ∈ U
3 mnuprdlem2.5 ⊢ φ → ¬ A = ∅
4 mnuprdlem2.8 ⊢ φ → ∀ i ∈ ∅ ∅ ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w
5 eleq1 ⊢ i = ∅ → i ∈ u ↔ ∅ ∈ u
6 5 anbi1d ⊢ i = ∅ → i ∈ u ∧ ⋃ u ⊆ w ↔ ∅ ∈ u ∧ ⋃ u ⊆ w
7 6 rexbidv ⊢ i = ∅ → ∃ u ∈ F i ∈ u ∧ ⋃ u ⊆ w ↔ ∃ u ∈ F ∅ ∈ u ∧ ⋃ u ⊆ w
8 p0ex ⊢ ∅ ∈ V
9 8 prid2 ⊢ ∅ ∈ ∅ ∅
10 9 a1i ⊢ φ → ∅ ∈ ∅ ∅
11 7 4 10 rspcdva ⊢ φ → ∃ u ∈ F ∅ ∈ u ∧ ⋃ u ⊆ w
12 simpl ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → φ
13 simprl ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → a ∈ F
14 simpr ⊢ φ ∧ ∅ ∈ a → ∅ ∈ a
15 0nep0 ⊢ ∅ ≠ ∅
16 15 necomi ⊢ ∅ ≠ ∅
17 16 a1i ⊢ φ → ∅ ≠ ∅
18 0ex ⊢ ∅ ∈ V
19 18 sneqr ⊢ ∅ = A → ∅ = A
20 19 eqcomd ⊢ ∅ = A → A = ∅
21 3 20 nsyl ⊢ φ → ¬ ∅ = A
22 21 neqned ⊢ φ → ∅ ≠ A
23 17 22 nelprd ⊢ φ → ¬ ∅ ∈ ∅ A
24 23 adantr ⊢ φ ∧ ∅ ∈ a → ¬ ∅ ∈ ∅ A
25 14 24 elnelneqd ⊢ φ ∧ ∅ ∈ a → ¬ a = ∅ A
26 25 adantrr ⊢ φ ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → ¬ a = ∅ A
27 26 adantrl ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → ¬ a = ∅ A
28 elpri ⊢ a ∈ ∅ A ∅ B → a = ∅ A ∨ a = ∅ B
29 28 1 eleq2s ⊢ a ∈ F → a = ∅ A ∨ a = ∅ B
30 29 ord ⊢ a ∈ F → ¬ a = ∅ A → a = ∅ B
31 13 27 30 sylc ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → a = ∅ B
32 31 unieqd ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → ⋃ a = ⋃ ∅ B
33 snex ⊢ B ∈ V
34 8 33 unipr ⊢ ⋃ ∅ B = ∅ ∪ B
35 df-pr ⊢ ∅ B = ∅ ∪ B
36 34 35 eqtr4i ⊢ ⋃ ∅ B = ∅ B
37 32 36 eqtrdi ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → ⋃ a = ∅ B
38 simprrr ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → ⋃ a ⊆ w
39 37 38 eqsstrrd ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → ∅ B ⊆ w
40 prssg ⊢ ∅ ∈ V ∧ B ∈ U → ∅ ∈ w ∧ B ∈ w ↔ ∅ B ⊆ w
41 18 2 40 sylancr ⊢ φ → ∅ ∈ w ∧ B ∈ w ↔ ∅ B ⊆ w
42 41 biimprd ⊢ φ → ∅ B ⊆ w → ∅ ∈ w ∧ B ∈ w
43 12 39 42 sylc ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → ∅ ∈ w ∧ B ∈ w
44 43 simprd ⊢ φ ∧ a ∈ F ∧ ∅ ∈ a ∧ ⋃ a ⊆ w → B ∈ w
45 eleq2w ⊢ u = a → ∅ ∈ u ↔ ∅ ∈ a
46 unieq ⊢ u = a → ⋃ u = ⋃ a
47 46 sseq1d ⊢ u = a → ⋃ u ⊆ w ↔ ⋃ a ⊆ w
48 45 47 anbi12d ⊢ u = a → ∅ ∈ u ∧ ⋃ u ⊆ w ↔ ∅ ∈ a ∧ ⋃ a ⊆ w
49 11 44 48 rexlimddvcbvw ⊢ φ → B ∈ w