Theorem mnuprdlem3

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

	Ref	Expression
Hypotheses	mnuprdlem3.1	⊢ 𝐹 = { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } }
	mnuprdlem3.9	⊢ Ⅎ 𝑖 𝜑
Assertion	mnuprdlem3	⊢ ( 𝜑 → ∀ 𝑖 ∈ { ∅ , { ∅ } } ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 )

Proof

Step	Hyp	Ref	Expression
1		mnuprdlem3.1	⊢ 𝐹 = { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } }
2		mnuprdlem3.9	⊢ Ⅎ 𝑖 𝜑
3		elpri	⊢ ( 𝑖 ∈ { ∅ , { ∅ } } → ( 𝑖 = ∅ ∨ 𝑖 = { ∅ } ) )
4		0ex	⊢ ∅ ∈ V
5	4	prid1	⊢ ∅ ∈ { ∅ , { 𝐴 } }
6	5	a1i	⊢ ( ( ( 𝜑 ∧ 𝑖 = ∅ ) ∧ 𝑎 = { ∅ , { 𝐴 } } ) → ∅ ∈ { ∅ , { 𝐴 } } )
7		simplr	⊢ ( ( ( 𝜑 ∧ 𝑖 = ∅ ) ∧ 𝑎 = { ∅ , { 𝐴 } } ) → 𝑖 = ∅ )
8		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 = ∅ ) ∧ 𝑎 = { ∅ , { 𝐴 } } ) → 𝑎 = { ∅ , { 𝐴 } } )
9	6 7 8	3eltr4d	⊢ ( ( ( 𝜑 ∧ 𝑖 = ∅ ) ∧ 𝑎 = { ∅ , { 𝐴 } } ) → 𝑖 ∈ 𝑎 )
10		prex	⊢ { ∅ , { 𝐴 } } ∈ V
11	10	prid1	⊢ { ∅ , { 𝐴 } } ∈ { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } }
12	11 1	eleqtrri	⊢ { ∅ , { 𝐴 } } ∈ 𝐹
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝑖 = ∅ ) → { ∅ , { 𝐴 } } ∈ 𝐹 )
14	9 13	rspcime	⊢ ( ( 𝜑 ∧ 𝑖 = ∅ ) → ∃ 𝑎 ∈ 𝐹 𝑖 ∈ 𝑎 )
15		p0ex	⊢ { ∅ } ∈ V
16	15	prid1	⊢ { ∅ } ∈ { { ∅ } , { 𝐵 } }
17	16	a1i	⊢ ( ( ( 𝜑 ∧ 𝑖 = { ∅ } ) ∧ 𝑎 = { { ∅ } , { 𝐵 } } ) → { ∅ } ∈ { { ∅ } , { 𝐵 } } )
18		simplr	⊢ ( ( ( 𝜑 ∧ 𝑖 = { ∅ } ) ∧ 𝑎 = { { ∅ } , { 𝐵 } } ) → 𝑖 = { ∅ } )
19		simpr	⊢ ( ( ( 𝜑 ∧ 𝑖 = { ∅ } ) ∧ 𝑎 = { { ∅ } , { 𝐵 } } ) → 𝑎 = { { ∅ } , { 𝐵 } } )
20	17 18 19	3eltr4d	⊢ ( ( ( 𝜑 ∧ 𝑖 = { ∅ } ) ∧ 𝑎 = { { ∅ } , { 𝐵 } } ) → 𝑖 ∈ 𝑎 )
21		prex	⊢ { { ∅ } , { 𝐵 } } ∈ V
22	21	prid2	⊢ { { ∅ } , { 𝐵 } } ∈ { { ∅ , { 𝐴 } } , { { ∅ } , { 𝐵 } } }
23	22 1	eleqtrri	⊢ { { ∅ } , { 𝐵 } } ∈ 𝐹
24	23	a1i	⊢ ( ( 𝜑 ∧ 𝑖 = { ∅ } ) → { { ∅ } , { 𝐵 } } ∈ 𝐹 )
25	20 24	rspcime	⊢ ( ( 𝜑 ∧ 𝑖 = { ∅ } ) → ∃ 𝑎 ∈ 𝐹 𝑖 ∈ 𝑎 )
26	14 25	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑖 = ∅ ∨ 𝑖 = { ∅ } ) ) → ∃ 𝑎 ∈ 𝐹 𝑖 ∈ 𝑎 )
27	3 26	sylan2	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { ∅ , { ∅ } } ) → ∃ 𝑎 ∈ 𝐹 𝑖 ∈ 𝑎 )
28		elequ2	⊢ ( 𝑎 = 𝑣 → ( 𝑖 ∈ 𝑎 ↔ 𝑖 ∈ 𝑣 ) )
29	28	cbvrexvw	⊢ ( ∃ 𝑎 ∈ 𝐹 𝑖 ∈ 𝑎 ↔ ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 )
30	27 29	sylib	⊢ ( ( 𝜑 ∧ 𝑖 ∈ { ∅ , { ∅ } } ) → ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 )
31	30	ex	⊢ ( 𝜑 → ( 𝑖 ∈ { ∅ , { ∅ } } → ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 ) )
32	2 31	ralrimi	⊢ ( 𝜑 → ∀ 𝑖 ∈ { ∅ , { ∅ } } ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 )