Theorem mnuprdlem3 45461

Description: Lemma for mnuprd 45463. (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 4608	. . . . 5 ⊢ (𝑖 ∈ {∅, {∅}} → (𝑖 = ∅ ∨ 𝑖 = {∅}))
3		0ex 5265	. . . . . . . . . 10 ⊢ ∅ ∈ V
4	3	prid1 4723	. . . . . . . . 9 ⊢ ∅ ∈ {∅, {𝐴}}
5	4	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → ∅ ∈ {∅, {𝐴}})
6		simplr 781	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 = ∅)
7		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑎 = {∅, {𝐴}})
8	5, 6, 7	3eltr4d 2879	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 ∈ 𝑎)
9		prex 5401	. . . . . . . . . 10 ⊢ {∅, {𝐴}} ∈ V
10	9	prid1 4723	. . . . . . . . 9 ⊢ {∅, {𝐴}} ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}}
11		mnuprdlem3.1	. . . . . . . . 9 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
12	10, 11	eleqtrri 2863	. . . . . . . 8 ⊢ {∅, {𝐴}} ∈ 𝐹
13	12	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = ∅) → {∅, {𝐴}} ∈ 𝐹)
14	8, 13	rspcime 3585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = ∅) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
15		snex 5402	. . . . . . . . . 10 ⊢ {∅} ∈ V
16	15	prid1 4723	. . . . . . . . 9 ⊢ {∅} ∈ {{∅}, {𝐵}}
17	16	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → {∅} ∈ {{∅}, {𝐵}})
18		simplr 781	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 = {∅})
19		simpr 490	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑎 = {{∅}, {𝐵}})
20	17, 18, 19	3eltr4d 2879	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 ∈ 𝑎)
21		prex 5401	. . . . . . . . . 10 ⊢ {{∅}, {𝐵}} ∈ V
22	21	prid2 4724	. . . . . . . . 9 ⊢ {{∅}, {𝐵}} ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}}
23	22, 11	eleqtrri 2863	. . . . . . . 8 ⊢ {{∅}, {𝐵}} ∈ 𝐹
24	23	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = {∅}) → {{∅}, {𝐵}} ∈ 𝐹)
25	20, 24	rspcime 3585	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = {∅}) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
26	14, 25	jaodan 972	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = ∅ ∨ 𝑖 = {∅})) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
27	2, 26	sylan2 605	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
28		elequ2 2162	. . . . 5 ⊢ (𝑎 = 𝑣 → (𝑖 ∈ 𝑎 ↔ 𝑖 ∈ 𝑣))
29	28	cbvrexvw 3245	. . . 4 ⊢ (∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎 ↔ ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
30	27, 29	sylib 221	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) → ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
31	30	ex 418	. 2 ⊢ (𝜑 → (𝑖 ∈ {∅, {∅}} → ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣))
32	1, 31	ralrimi 3264	1 ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570  Ⅎwnf 1816   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090  ∅c0 4281  {csn 4588  {cpr 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pr 5396

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-v 3456  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591

This theorem is used by:  mnuprdlem4  45462