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 ∈ F i ∈ 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 ∈ F i ∈ a
15 snex ⊢ ∅ ∈ 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 ∈ F i ∈ a
26 14 25 jaodan ⊢ φ ∧ i = ∅ ∨ i = ∅ → ∃ a ∈ F i ∈ a
27 3 26 sylan2 ⊢ φ ∧ i ∈ ∅ ∅ → ∃ a ∈ F i ∈ a
28 elequ2 ⊢ a = v → i ∈ a ↔ i ∈ v
29 28 cbvrexvw ⊢ ∃ a ∈ F i ∈ a ↔ ∃ v ∈ F i ∈ v
30 27 29 sylib ⊢ φ ∧ i ∈ ∅ ∅ → ∃ v ∈ F i ∈ v
31 30 ex ⊢ φ → i ∈ ∅ ∅ → ∃ v ∈ F i ∈ v
32 2 31 ralrimi ⊢ φ → ∀ i ∈ ∅ ∅ ∃ v ∈ F i ∈ v