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∈Fi∈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∈Fi∈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∈Fi∈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