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