Theorem mnuprdlem3 41781

Description: Lemma for mnuprd 41783. (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 4580	. . . . 5 ⊢ (𝑖 ∈ {∅, {∅}} → (𝑖 = ∅ ∨ 𝑖 = {∅}))
3		0ex 5226	. . . . . . . . . 10 ⊢ ∅ ∈ V
4	3	prid1 4695	. . . . . . . . 9 ⊢ ∅ ∈ {∅, {𝐴}}
5	4	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → ∅ ∈ {∅, {𝐴}})
6		simplr 765	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 = ∅)
7		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑎 = {∅, {𝐴}})
8	5, 6, 7	3eltr4d 2854	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 ∈ 𝑎)
9		prex 5350	. . . . . . . . . 10 ⊢ {∅, {𝐴}} ∈ V
10	9	prid1 4695	. . . . . . . . 9 ⊢ {∅, {𝐴}} ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}}
11		mnuprdlem3.1	. . . . . . . . 9 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
12	10, 11	eleqtrri 2838	. . . . . . . 8 ⊢ {∅, {𝐴}} ∈ 𝐹
13	12	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = ∅) → {∅, {𝐴}} ∈ 𝐹)
14	8, 13	rspcime 3556	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = ∅) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
15		p0ex 5302	. . . . . . . . . 10 ⊢ {∅} ∈ V
16	15	prid1 4695	. . . . . . . . 9 ⊢ {∅} ∈ {{∅}, {𝐵}}
17	16	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → {∅} ∈ {{∅}, {𝐵}})
18		simplr 765	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 = {∅})
19		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑎 = {{∅}, {𝐵}})
20	17, 18, 19	3eltr4d 2854	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 ∈ 𝑎)
21		prex 5350	. . . . . . . . . 10 ⊢ {{∅}, {𝐵}} ∈ V
22	21	prid2 4696	. . . . . . . . 9 ⊢ {{∅}, {𝐵}} ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}}
23	22, 11	eleqtrri 2838	. . . . . . . 8 ⊢ {{∅}, {𝐵}} ∈ 𝐹
24	23	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = {∅}) → {{∅}, {𝐵}} ∈ 𝐹)
25	20, 24	rspcime 3556	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = {∅}) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
26	14, 25	jaodan 954	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = ∅ ∨ 𝑖 = {∅})) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
27	2, 26	sylan2 592	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
28		elequ2 2123	. . . . 5 ⊢ (𝑎 = 𝑣 → (𝑖 ∈ 𝑎 ↔ 𝑖 ∈ 𝑣))
29	28	cbvrexvw 3373	. . . 4 ⊢ (∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎 ↔ ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
30	27, 29	sylib 217	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) → ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
31	30	ex 412	. 2 ⊢ (𝜑 → (𝑖 ∈ {∅, {∅}} → ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣))
32	1, 31	ralrimi 3139	1 ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 843   = wceq 1539  Ⅎwnf 1787   ∈ wcel 2108  ∀wral 3063  ∃wrex 3064  ∅c0 4253  {csn 4558  {cpr 4560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rex 3069  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-pw 4532  df-sn 4559  df-pr 4561

This theorem is referenced by:  mnuprdlem4  41782