Metamath Proof Explorer

Theorem mnuprdlem3

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

Ref Expression
Hypotheses mnuprdlem3.1 ⊢F=∅A∅B
mnuprdlem3.9 ⊢Ⅎiφ
Assertion mnuprdlem3 ⊢φ→∀i∈∅∅∃v∈Fi∈v

Proof

Step Hyp Ref Expression
1 mnuprdlem3.1 ⊢F=∅A∅B
2 mnuprdlem3.9 ⊢Ⅎiφ
3 elpri ⊢i∈∅∅→i=∅∨i=∅
4 0ex ⊢∅∈V
5 4 prid1 ⊢∅∈∅A
6 5 a1i ⊢φ∧i=∅∧a=∅A→∅∈∅A
7 simplr ⊢φ∧i=∅∧a=∅A→i=∅
8 simpr ⊢φ∧i=∅∧a=∅A→a=∅A
9 6 7 8 3eltr4d ⊢φ∧i=∅∧a=∅A→i∈a
10 prex ⊢∅A∈V
11 10 prid1 ⊢∅A∈∅A∅B
12 11 1 eleqtrri ⊢∅A∈F
13 12 a1i ⊢φ∧i=∅→∅A∈F
14 9 13 rspcime ⊢φ∧i=∅→∃a∈Fi∈a
15 p0ex ⊢∅∈V
16 15 prid1 ⊢∅∈∅B
17 16 a1i ⊢φ∧i=∅∧a=∅B→∅∈∅B
18 simplr ⊢φ∧i=∅∧a=∅B→i=∅
19 simpr ⊢φ∧i=∅∧a=∅B→a=∅B
20 17 18 19 3eltr4d ⊢φ∧i=∅∧a=∅B→i∈a
21 prex ⊢∅B∈V
22 21 prid2 ⊢∅B∈∅A∅B
23 22 1 eleqtrri ⊢∅B∈F
24 23 a1i ⊢φ∧i=∅→∅B∈F
25 20 24 rspcime ⊢φ∧i=∅→∃a∈Fi∈a
26 14 25 jaodan ⊢φ∧i=∅∨i=∅→∃a∈Fi∈a
27 3 26 sylan2 ⊢φ∧i∈∅∅→∃a∈Fi∈a
28 elequ2 ⊢a=v→i∈a↔i∈v
29 28 cbvrexvw ⊢∃a∈Fi∈a↔∃v∈Fi∈v
30 27 29 sylib ⊢φ∧i∈∅∅→∃v∈Fi∈v
31 30 ex ⊢φ→i∈∅∅→∃v∈Fi∈v
32 2 31 ralrimi ⊢φ→∀i∈∅∅∃v∈Fi∈v