Theorem mnuprdlem1 45517

Description: Lemma for mnuprd 45521. (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 2852	. . . . 5 ⊢ (𝑖 = ∅ → (𝑖 ∈ 𝑢 ↔ ∅ ∈ 𝑢))
2	1	anbi1d 643	. . . 4 ⊢ (𝑖 = ∅ → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
3	2	rexbidv 3190	. . 3 ⊢ (𝑖 = ∅ → (∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		mnuprdlem1.8	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
5		0ex 5267	. . . . 5 ⊢ ∅ ∈ V
6	5	prid1 4725	. . . 4 ⊢ ∅ ∈ {∅, {∅}}
7	6	a1i 11	. . 3 ⊢ (𝜑 → ∅ ∈ {∅, {∅}})
8	3, 4, 7	rspcdva 3581	. 2 ⊢ (𝜑 → ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
9		mnuprdlem1.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
10	9	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑈)
11		simprl 783	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 ∈ 𝐹)
12		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ∅ ∈ 𝑎)
13		0nep0 5326	. . . . . . . . . . . . 13 ⊢ ∅ ≠ {∅}
14	13	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {∅})
15		mnuprdlem1.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
16	15	snn0d 4738	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐵} ≠ ∅)
17	16	necomd 3014	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {𝐵})
18	14, 17	nelprd 4619	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∅ ∈ {{∅}, {𝐵}})
19	18	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ ∅ ∈ {{∅}, {𝐵}})
20	12, 19	elnelneqd 3058	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ 𝑎 = {{∅}, {𝐵}})
21	20	adantrr 730	. . . . . . . 8 ⊢ ((𝜑 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)) → ¬ 𝑎 = {{∅}, {𝐵}})
22	21	adantrl 729	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ¬ 𝑎 = {{∅}, {𝐵}})
23		elpri 4608	. . . . . . . . . 10 ⊢ (𝑎 ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}} → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
24		mnuprdlem1.1	. . . . . . . . . 10 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
25	23, 24	eleq2s 2882	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
26	25	orcomd 885	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {{∅}, {𝐵}} ∨ 𝑎 = {∅, {𝐴}}))
27	26	ord 878	. . . . . . 7 ⊢ (𝑎 ∈ 𝐹 → (¬ 𝑎 = {{∅}, {𝐵}} → 𝑎 = {∅, {𝐴}}))
28	11, 22, 27	sylc 66	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 = {∅, {𝐴}})
29	28	unieqd 4885	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = ∪ {∅, {𝐴}})
30		snex 5404	. . . . . . 7 ⊢ {𝐴} ∈ V
31	5, 30	unipr 4889	. . . . . 6 ⊢ ∪ {∅, {𝐴}} = (∅ ∪ {𝐴})
32		uncom 4160	. . . . . 6 ⊢ (∅ ∪ {𝐴}) = ({𝐴} ∪ ∅)
33		un0 4347	. . . . . 6 ⊢ ({𝐴} ∪ ∅) = {𝐴}
34	31, 32, 33	3eqtri 2790	. . . . 5 ⊢ ∪ {∅, {𝐴}} = {𝐴}
35	29, 34	eqtrdi 2814	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = {𝐴})
36		simprrr 794	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 ⊆ 𝑤)
37	35, 36	eqsstrrd 3948	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → {𝐴} ⊆ 𝑤)
38		snssg 4746	. . . 4 ⊢ (𝐴 ∈ 𝑈 → (𝐴 ∈ 𝑤 ↔ {𝐴} ⊆ 𝑤))
39	38	biimprd 251	. . 3 ⊢ (𝐴 ∈ 𝑈 → ({𝐴} ⊆ 𝑤 → 𝐴 ∈ 𝑤))
40	10, 37, 39	sylc 66	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑤)
41		eleq2w 2848	. . 3 ⊢ (𝑢 = 𝑎 → (∅ ∈ 𝑢 ↔ ∅ ∈ 𝑎))
42		unieq 4883	. . . 4 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
43	42	sseq1d 3944	. . 3 ⊢ (𝑢 = 𝑎 → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤))
44	41, 43	anbi12d 644	. 2 ⊢ (𝑢 = 𝑎 → ((∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)))
45	8, 40, 44	rexlimddvcbvw 45465	1 ⊢ (𝜑 → 𝐴 ∈ 𝑤)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2147   ≠ wne 2959  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900   ∪ cun 4152  ∅c0 4281  {csn 4588  {cpr 4590  ∪ cuni 4872

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-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

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

This theorem is used by:  mnuprdlem4  45520