Theorem mnuprdlem3 44265

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

Hypotheses

Ref	Expression
mnuprdlem3.1	⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
mnuprdlem3.9	⊢ Ⅎ𝑖𝜑

Assertion

Ref	Expression
mnuprdlem3	⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)

Distinct variable groups:   𝑣,𝑖   𝑣,𝐹

Allowed substitution hints:   𝜑(𝑣,𝑖)   𝐴(𝑣,𝑖)   𝐵(𝑣,𝑖)   𝐹(𝑖)

Proof of Theorem mnuprdlem3

Dummy variable 𝑎 is distinct from all other variables.

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540  Ⅎwnf 1783   ∈ wcel 2109  ∀wral 3052  ∃wrex 3061  ∅c0 4313  {csn 4606  {cpr 4608

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-pw 4582  df-sn 4607  df-pr 4609

This theorem is referenced by:  mnuprdlem4  44266