Theorem mnuprdlem3

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

	Ref	Expression
Hypotheses	mnuprdlem3.1	|- F = { { (/) , { A } } , { { (/) } , { B } } }
	mnuprdlem3.9	|- F/ i ph
Assertion	mnuprdlem3	|- ( ph -> A. i e. { (/) , { (/) } } E. v e. F i e. v )

Proof

Step	Hyp	Ref	Expression
1		mnuprdlem3.1	|- F = { { (/) , { A } } , { { (/) } , { B } } }
2		mnuprdlem3.9	|- F/ i ph
3		elpri	|- ( i e. { (/) , { (/) } } -> ( i = (/) \/ i = { (/) } ) )
4		0ex	|- (/) e. _V
5	4	prid1	|- (/) e. { (/) , { A } }
6	5	a1i	|- ( ( ( ph /\ i = (/) ) /\ a = { (/) , { A } } ) -> (/) e. { (/) , { A } } )
7		simplr	|- ( ( ( ph /\ i = (/) ) /\ a = { (/) , { A } } ) -> i = (/) )
8		simpr	|- ( ( ( ph /\ i = (/) ) /\ a = { (/) , { A } } ) -> a = { (/) , { A } } )
9	6 7 8	3eltr4d	|- ( ( ( ph /\ i = (/) ) /\ a = { (/) , { A } } ) -> i e. a )
10		prex	|- { (/) , { A } } e. _V
11	10	prid1	|- { (/) , { A } } e. { { (/) , { A } } , { { (/) } , { B } } }
12	11 1	eleqtrri	|- { (/) , { A } } e. F
13	12	a1i	|- ( ( ph /\ i = (/) ) -> { (/) , { A } } e. F )
14	9 13	rspcime	|- ( ( ph /\ i = (/) ) -> E. a e. F i e. a )
15		p0ex	|- { (/) } e. _V
16	15	prid1	|- { (/) } e. { { (/) } , { B } }
17	16	a1i	|- ( ( ( ph /\ i = { (/) } ) /\ a = { { (/) } , { B } } ) -> { (/) } e. { { (/) } , { B } } )
18		simplr	|- ( ( ( ph /\ i = { (/) } ) /\ a = { { (/) } , { B } } ) -> i = { (/) } )
19		simpr	|- ( ( ( ph /\ i = { (/) } ) /\ a = { { (/) } , { B } } ) -> a = { { (/) } , { B } } )
20	17 18 19	3eltr4d	|- ( ( ( ph /\ i = { (/) } ) /\ a = { { (/) } , { B } } ) -> i e. a )
21		prex	|- { { (/) } , { B } } e. _V
22	21	prid2	|- { { (/) } , { B } } e. { { (/) , { A } } , { { (/) } , { B } } }
23	22 1	eleqtrri	|- { { (/) } , { B } } e. F
24	23	a1i	|- ( ( ph /\ i = { (/) } ) -> { { (/) } , { B } } e. F )
25	20 24	rspcime	|- ( ( ph /\ i = { (/) } ) -> E. a e. F i e. a )
26	14 25	jaodan	|- ( ( ph /\ ( i = (/) \/ i = { (/) } ) ) -> E. a e. F i e. a )
27	3 26	sylan2	|- ( ( ph /\ i e. { (/) , { (/) } } ) -> E. a e. F i e. a )
28		elequ2	|- ( a = v -> ( i e. a <-> i e. v ) )
29	28	cbvrexvw	|- ( E. a e. F i e. a <-> E. v e. F i e. v )
30	27 29	sylib	|- ( ( ph /\ i e. { (/) , { (/) } } ) -> E. v e. F i e. v )
31	30	ex	|- ( ph -> ( i e. { (/) , { (/) } } -> E. v e. F i e. v ) )
32	2 31	ralrimi	|- ( ph -> A. i e. { (/) , { (/) } } E. v e. F i e. v )