Theorem mnuprdlem1 42124

Description: Lemma for mnuprd 42128. (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 2825	. . . . 5 ⊢ (𝑖 = ∅ → (𝑖 ∈ 𝑢 ↔ ∅ ∈ 𝑢))
2	1	anbi1d 630	. . . 4 ⊢ (𝑖 = ∅ → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
3	2	rexbidv 3172	. . 3 ⊢ (𝑖 = ∅ → (∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		mnuprdlem1.8	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
5		0ex 5246	. . . . 5 ⊢ ∅ ∈ V
6	5	prid1 4708	. . . 4 ⊢ ∅ ∈ {∅, {∅}}
7	6	a1i 11	. . 3 ⊢ (𝜑 → ∅ ∈ {∅, {∅}})
8	3, 4, 7	rspcdva 3571	. 2 ⊢ (𝜑 → ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
9		mnuprdlem1.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
10	9	adantr 481	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑈)
11		simprl 768	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 ∈ 𝐹)
12		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ∅ ∈ 𝑎)
13		0nep0 5295	. . . . . . . . . . . . 13 ⊢ ∅ ≠ {∅}
14	13	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {∅})
15		mnuprdlem1.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
16	15	snn0d 4721	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐵} ≠ ∅)
17	16	necomd 2997	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {𝐵})
18	14, 17	nelprd 4602	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∅ ∈ {{∅}, {𝐵}})
19	18	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ ∅ ∈ {{∅}, {𝐵}})
20	12, 19	elnelneqd 42047	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ 𝑎 = {{∅}, {𝐵}})
21	20	adantrr 714	. . . . . . . 8 ⊢ ((𝜑 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)) → ¬ 𝑎 = {{∅}, {𝐵}})
22	21	adantrl 713	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ¬ 𝑎 = {{∅}, {𝐵}})
23		elpri 4593	. . . . . . . . . 10 ⊢ (𝑎 ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}} → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
24		mnuprdlem1.1	. . . . . . . . . 10 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
25	23, 24	eleq2s 2856	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
26	25	orcomd 868	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {{∅}, {𝐵}} ∨ 𝑎 = {∅, {𝐴}}))
27	26	ord 861	. . . . . . 7 ⊢ (𝑎 ∈ 𝐹 → (¬ 𝑎 = {{∅}, {𝐵}} → 𝑎 = {∅, {𝐴}}))
28	11, 22, 27	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 = {∅, {𝐴}})
29	28	unieqd 4864	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = ∪ {∅, {𝐴}})
30		snex 5369	. . . . . . 7 ⊢ {𝐴} ∈ V
31	5, 30	unipr 4868	. . . . . 6 ⊢ ∪ {∅, {𝐴}} = (∅ ∪ {𝐴})
32		uncom 4098	. . . . . 6 ⊢ (∅ ∪ {𝐴}) = ({𝐴} ∪ ∅)
33		un0 4335	. . . . . 6 ⊢ ({𝐴} ∪ ∅) = {𝐴}
34	31, 32, 33	3eqtri 2769	. . . . 5 ⊢ ∪ {∅, {𝐴}} = {𝐴}
35	29, 34	eqtrdi 2793	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = {𝐴})
36		simprrr 779	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 ⊆ 𝑤)
37	35, 36	eqsstrrd 3970	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → {𝐴} ⊆ 𝑤)
38		snssg 4729	. . . 4 ⊢ (𝐴 ∈ 𝑈 → (𝐴 ∈ 𝑤 ↔ {𝐴} ⊆ 𝑤))
39	38	biimprd 247	. . 3 ⊢ (𝐴 ∈ 𝑈 → ({𝐴} ⊆ 𝑤 → 𝐴 ∈ 𝑤))
40	10, 37, 39	sylc 65	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑤)
41		eleq2w 2821	. . 3 ⊢ (𝑢 = 𝑎 → (∅ ∈ 𝑢 ↔ ∅ ∈ 𝑎))
42		unieq 4861	. . . 4 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
43	42	sseq1d 3962	. . 3 ⊢ (𝑢 = 𝑎 → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤))
44	41, 43	anbi12d 631	. 2 ⊢ (𝑢 = 𝑎 → ((∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)))
45	8, 40, 44	rexlimddvcbvw 42051	1 ⊢ (𝜑 → 𝐴 ∈ 𝑤)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   ∨ wo 844   = wceq 1540   ∈ wcel 2105   ≠ wne 2941  ∀wral 3062  ∃wrex 3071   ∪ cun 3895   ⊆ wss 3897  ∅c0 4267  {csn 4571  {cpr 4573  ∪ cuni 4850

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2708  ax-sep 5238  ax-nul 5245  ax-pr 5367

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2715  df-cleq 2729  df-clel 2815  df-ne 2942  df-ral 3063  df-rex 3072  df-v 3443  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4268  df-sn 4572  df-pr 4574  df-uni 4851

This theorem is referenced by:  mnuprdlem4  42127