Theorem mnuprdlem3 40659

Description: Lemma for mnuprd 40661. (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 4589	. . . . 5 ⊢ (𝑖 ∈ {∅, {∅}} → (𝑖 = ∅ ∨ 𝑖 = {∅}))
3		0ex 5211	. . . . . . . . . 10 ⊢ ∅ ∈ V
4	3	prid1 4698	. . . . . . . . 9 ⊢ ∅ ∈ {∅, {𝐴}}
5	4	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → ∅ ∈ {∅, {𝐴}})
6		simplr 767	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 = ∅)
7		simpr 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑎 = {∅, {𝐴}})
8	5, 6, 7	3eltr4d 2928	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 ∈ 𝑎)
9		prex 5333	. . . . . . . . . 10 ⊢ {∅, {𝐴}} ∈ V
10	9	prid1 4698	. . . . . . . . 9 ⊢ {∅, {𝐴}} ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}}
11		mnuprdlem3.1	. . . . . . . . 9 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
12	10, 11	eleqtrri 2912	. . . . . . . 8 ⊢ {∅, {𝐴}} ∈ 𝐹
13	12	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = ∅) → {∅, {𝐴}} ∈ 𝐹)
14	8, 13	rspcime 3627	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = ∅) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
15		p0ex 5285	. . . . . . . . . 10 ⊢ {∅} ∈ V
16	15	prid1 4698	. . . . . . . . 9 ⊢ {∅} ∈ {{∅}, {𝐵}}
17	16	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → {∅} ∈ {{∅}, {𝐵}})
18		simplr 767	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 = {∅})
19		simpr 487	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑎 = {{∅}, {𝐵}})
20	17, 18, 19	3eltr4d 2928	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 ∈ 𝑎)
21		prex 5333	. . . . . . . . . 10 ⊢ {{∅}, {𝐵}} ∈ V
22	21	prid2 4699	. . . . . . . . 9 ⊢ {{∅}, {𝐵}} ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}}
23	22, 11	eleqtrri 2912	. . . . . . . 8 ⊢ {{∅}, {𝐵}} ∈ 𝐹
24	23	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = {∅}) → {{∅}, {𝐵}} ∈ 𝐹)
25	20, 24	rspcime 3627	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = {∅}) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
26	14, 25	jaodan 954	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = ∅ ∨ 𝑖 = {∅})) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
27	2, 26	sylan2 594	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
28		elequ2 2129	. . . . 5 ⊢ (𝑎 = 𝑣 → (𝑖 ∈ 𝑎 ↔ 𝑖 ∈ 𝑣))
29	28	cbvrexvw 3450	. . . 4 ⊢ (∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎 ↔ ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
30	27, 29	sylib 220	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) → ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
31	30	ex 415	. 2 ⊢ (𝜑 → (𝑖 ∈ {∅, {∅}} → ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣))
32	1, 31	ralrimi 3216	1 ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843   = wceq 1537  Ⅎwnf 1784   ∈ wcel 2114  ∀wral 3138  ∃wrex 3139  ∅c0 4291  {csn 4567  {cpr 4569

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-pw 4541  df-sn 4568  df-pr 4570

This theorem is referenced by:  mnuprdlem4  40660