Theorem mnuprdlem1 44296

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

Hypotheses

Ref	Expression
mnuprdlem1.1	⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
mnuprdlem1.3	⊢ (𝜑 → 𝐴 ∈ 𝑈)
mnuprdlem1.4	⊢ (𝜑 → 𝐵 ∈ 𝑈)
mnuprdlem1.8	⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))

Assertion

Ref	Expression
mnuprdlem1	⊢ (𝜑 → 𝐴 ∈ 𝑤)

Distinct variable groups:   𝑤,𝑖,𝑢   𝑢,𝐹,𝑖

Allowed substitution hints:   𝜑(𝑤,𝑢,𝑖)   𝐴(𝑤,𝑢,𝑖)   𝐵(𝑤,𝑢,𝑖)   𝑈(𝑤,𝑢,𝑖)   𝐹(𝑤)

Proof of Theorem mnuprdlem1

Dummy variable 𝑎 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eleq1 2822	. . . . 5 ⊢ (𝑖 = ∅ → (𝑖 ∈ 𝑢 ↔ ∅ ∈ 𝑢))
2	1	anbi1d 631	. . . 4 ⊢ (𝑖 = ∅ → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
3	2	rexbidv 3164	. . 3 ⊢ (𝑖 = ∅ → (∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		mnuprdlem1.8	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
5		0ex 5277	. . . . 5 ⊢ ∅ ∈ V
6	5	prid1 4738	. . . 4 ⊢ ∅ ∈ {∅, {∅}}
7	6	a1i 11	. . 3 ⊢ (𝜑 → ∅ ∈ {∅, {∅}})
8	3, 4, 7	rspcdva 3602	. 2 ⊢ (𝜑 → ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
9		mnuprdlem1.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
10	9	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑈)
11		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 ∈ 𝐹)
12		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ∅ ∈ 𝑎)
13		0nep0 5328	. . . . . . . . . . . . 13 ⊢ ∅ ≠ {∅}
14	13	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {∅})
15		mnuprdlem1.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
16	15	snn0d 4751	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐵} ≠ ∅)
17	16	necomd 2987	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {𝐵})
18	14, 17	nelprd 4633	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∅ ∈ {{∅}, {𝐵}})
19	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ ∅ ∈ {{∅}, {𝐵}})
20	12, 19	elnelneqd 44226	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ 𝑎 = {{∅}, {𝐵}})
21	20	adantrr 717	. . . . . . . 8 ⊢ ((𝜑 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)) → ¬ 𝑎 = {{∅}, {𝐵}})
22	21	adantrl 716	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ¬ 𝑎 = {{∅}, {𝐵}})
23		elpri 4625	. . . . . . . . . 10 ⊢ (𝑎 ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}} → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
24		mnuprdlem1.1	. . . . . . . . . 10 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
25	23, 24	eleq2s 2852	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
26	25	orcomd 871	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {{∅}, {𝐵}} ∨ 𝑎 = {∅, {𝐴}}))
27	26	ord 864	. . . . . . 7 ⊢ (𝑎 ∈ 𝐹 → (¬ 𝑎 = {{∅}, {𝐵}} → 𝑎 = {∅, {𝐴}}))
28	11, 22, 27	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 = {∅, {𝐴}})
29	28	unieqd 4896	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = ∪ {∅, {𝐴}})
30		snex 5406	. . . . . . 7 ⊢ {𝐴} ∈ V
31	5, 30	unipr 4900	. . . . . 6 ⊢ ∪ {∅, {𝐴}} = (∅ ∪ {𝐴})
32		uncom 4133	. . . . . 6 ⊢ (∅ ∪ {𝐴}) = ({𝐴} ∪ ∅)
33		un0 4369	. . . . . 6 ⊢ ({𝐴} ∪ ∅) = {𝐴}
34	31, 32, 33	3eqtri 2762	. . . . 5 ⊢ ∪ {∅, {𝐴}} = {𝐴}
35	29, 34	eqtrdi 2786	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = {𝐴})
36		simprrr 781	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 ⊆ 𝑤)
37	35, 36	eqsstrrd 3994	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → {𝐴} ⊆ 𝑤)
38		snssg 4759	. . . 4 ⊢ (𝐴 ∈ 𝑈 → (𝐴 ∈ 𝑤 ↔ {𝐴} ⊆ 𝑤))
39	38	biimprd 248	. . 3 ⊢ (𝐴 ∈ 𝑈 → ({𝐴} ⊆ 𝑤 → 𝐴 ∈ 𝑤))
40	10, 37, 39	sylc 65	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑤)
41		eleq2w 2818	. . 3 ⊢ (𝑢 = 𝑎 → (∅ ∈ 𝑢 ↔ ∅ ∈ 𝑎))
42		unieq 4894	. . . 4 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
43	42	sseq1d 3990	. . 3 ⊢ (𝑢 = 𝑎 → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤))
44	41, 43	anbi12d 632	. 2 ⊢ (𝑢 = 𝑎 → ((∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)))
45	8, 40, 44	rexlimddvcbvw 44230	1 ⊢ (𝜑 → 𝐴 ∈ 𝑤)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  ∀wral 3051  ∃wrex 3060   ∪ cun 3924   ⊆ wss 3926  ∅c0 4308  {csn 4601  {cpr 4603  ∪ cuni 4883

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-ne 2933  df-ral 3052  df-rex 3061  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-sn 4602  df-pr 4604  df-uni 4884

This theorem is referenced by:  mnuprdlem4  44299