Theorem mnuprdlem3 44627

Description: Lemma for mnuprd 44629. (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 4606	. . . . 5 ⊢ (𝑖 ∈ {∅, {∅}} → (𝑖 = ∅ ∨ 𝑖 = {∅}))
3		0ex 5254	. . . . . . . . . 10 ⊢ ∅ ∈ V
4	3	prid1 4721	. . . . . . . . 9 ⊢ ∅ ∈ {∅, {𝐴}}
5	4	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → ∅ ∈ {∅, {𝐴}})
6		simplr 769	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 = ∅)
7		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑎 = {∅, {𝐴}})
8	5, 6, 7	3eltr4d 2852	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 = ∅) ∧ 𝑎 = {∅, {𝐴}}) → 𝑖 ∈ 𝑎)
9		prex 5384	. . . . . . . . . 10 ⊢ {∅, {𝐴}} ∈ V
10	9	prid1 4721	. . . . . . . . 9 ⊢ {∅, {𝐴}} ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}}
11		mnuprdlem3.1	. . . . . . . . 9 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
12	10, 11	eleqtrri 2836	. . . . . . . 8 ⊢ {∅, {𝐴}} ∈ 𝐹
13	12	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = ∅) → {∅, {𝐴}} ∈ 𝐹)
14	8, 13	rspcime 3583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = ∅) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
15		p0ex 5331	. . . . . . . . . 10 ⊢ {∅} ∈ V
16	15	prid1 4721	. . . . . . . . 9 ⊢ {∅} ∈ {{∅}, {𝐵}}
17	16	a1i 11	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → {∅} ∈ {{∅}, {𝐵}})
18		simplr 769	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 = {∅})
19		simpr 484	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑎 = {{∅}, {𝐵}})
20	17, 18, 19	3eltr4d 2852	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 = {∅}) ∧ 𝑎 = {{∅}, {𝐵}}) → 𝑖 ∈ 𝑎)
21		prex 5384	. . . . . . . . . 10 ⊢ {{∅}, {𝐵}} ∈ V
22	21	prid2 4722	. . . . . . . . 9 ⊢ {{∅}, {𝐵}} ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}}
23	22, 11	eleqtrri 2836	. . . . . . . 8 ⊢ {{∅}, {𝐵}} ∈ 𝐹
24	23	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑖 = {∅}) → {{∅}, {𝐵}} ∈ 𝐹)
25	20, 24	rspcime 3583	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 = {∅}) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
26	14, 25	jaodan 960	. . . . 5 ⊢ ((𝜑 ∧ (𝑖 = ∅ ∨ 𝑖 = {∅})) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
27	2, 26	sylan2 594	. . . 4 ⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) → ∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎)
28		elequ2 2129	. . . . 5 ⊢ (𝑎 = 𝑣 → (𝑖 ∈ 𝑎 ↔ 𝑖 ∈ 𝑣))
29	28	cbvrexvw 3217	. . . 4 ⊢ (∃𝑎 ∈ 𝐹 𝑖 ∈ 𝑎 ↔ ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
30	27, 29	sylib 218	. . 3 ⊢ ((𝜑 ∧ 𝑖 ∈ {∅, {∅}}) → ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
31	30	ex 412	. 2 ⊢ (𝜑 → (𝑖 ∈ {∅, {∅}} → ∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣))
32	1, 31	ralrimi 3236	1 ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848   = wceq 1542  Ⅎwnf 1785   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062  ∅c0 4287  {csn 4582  {cpr 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pow 5312  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-ral 3053  df-rex 3063  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-pw 4558  df-sn 4583  df-pr 4585

This theorem is referenced by:  mnuprdlem4  44628