Theorem mnuprdlem1 44268

Description: Lemma for mnuprd 44272. (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 2817	. . . . 5 ⊢ (𝑖 = ∅ → (𝑖 ∈ 𝑢 ↔ ∅ ∈ 𝑢))
2	1	anbi1d 631	. . . 4 ⊢ (𝑖 = ∅ → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
3	2	rexbidv 3158	. . 3 ⊢ (𝑖 = ∅ → (∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		mnuprdlem1.8	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
5		0ex 5265	. . . . 5 ⊢ ∅ ∈ V
6	5	prid1 4729	. . . 4 ⊢ ∅ ∈ {∅, {∅}}
7	6	a1i 11	. . 3 ⊢ (𝜑 → ∅ ∈ {∅, {∅}})
8	3, 4, 7	rspcdva 3592	. 2 ⊢ (𝜑 → ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
9		mnuprdlem1.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
10	9	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑈)
11		simprl 770	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 ∈ 𝐹)
12		simpr 484	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ∅ ∈ 𝑎)
13		0nep0 5316	. . . . . . . . . . . . 13 ⊢ ∅ ≠ {∅}
14	13	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {∅})
15		mnuprdlem1.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
16	15	snn0d 4742	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐵} ≠ ∅)
17	16	necomd 2981	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {𝐵})
18	14, 17	nelprd 4624	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∅ ∈ {{∅}, {𝐵}})
19	18	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ ∅ ∈ {{∅}, {𝐵}})
20	12, 19	elnelneqd 44198	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ 𝑎 = {{∅}, {𝐵}})
21	20	adantrr 717	. . . . . . . 8 ⊢ ((𝜑 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)) → ¬ 𝑎 = {{∅}, {𝐵}})
22	21	adantrl 716	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ¬ 𝑎 = {{∅}, {𝐵}})
23		elpri 4616	. . . . . . . . . 10 ⊢ (𝑎 ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}} → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
24		mnuprdlem1.1	. . . . . . . . . 10 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
25	23, 24	eleq2s 2847	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
26	25	orcomd 871	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {{∅}, {𝐵}} ∨ 𝑎 = {∅, {𝐴}}))
27	26	ord 864	. . . . . . 7 ⊢ (𝑎 ∈ 𝐹 → (¬ 𝑎 = {{∅}, {𝐵}} → 𝑎 = {∅, {𝐴}}))
28	11, 22, 27	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 = {∅, {𝐴}})
29	28	unieqd 4887	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = ∪ {∅, {𝐴}})
30		snex 5394	. . . . . . 7 ⊢ {𝐴} ∈ V
31	5, 30	unipr 4891	. . . . . 6 ⊢ ∪ {∅, {𝐴}} = (∅ ∪ {𝐴})
32		uncom 4124	. . . . . 6 ⊢ (∅ ∪ {𝐴}) = ({𝐴} ∪ ∅)
33		un0 4360	. . . . . 6 ⊢ ({𝐴} ∪ ∅) = {𝐴}
34	31, 32, 33	3eqtri 2757	. . . . 5 ⊢ ∪ {∅, {𝐴}} = {𝐴}
35	29, 34	eqtrdi 2781	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = {𝐴})
36		simprrr 781	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 ⊆ 𝑤)
37	35, 36	eqsstrrd 3985	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → {𝐴} ⊆ 𝑤)
38		snssg 4750	. . . 4 ⊢ (𝐴 ∈ 𝑈 → (𝐴 ∈ 𝑤 ↔ {𝐴} ⊆ 𝑤))
39	38	biimprd 248	. . 3 ⊢ (𝐴 ∈ 𝑈 → ({𝐴} ⊆ 𝑤 → 𝐴 ∈ 𝑤))
40	10, 37, 39	sylc 65	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑤)
41		eleq2w 2813	. . 3 ⊢ (𝑢 = 𝑎 → (∅ ∈ 𝑢 ↔ ∅ ∈ 𝑎))
42		unieq 4885	. . . 4 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
43	42	sseq1d 3981	. . 3 ⊢ (𝑢 = 𝑎 → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤))
44	41, 43	anbi12d 632	. 2 ⊢ (𝑢 = 𝑎 → ((∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)))
45	8, 40, 44	rexlimddvcbvw 44202	1 ⊢ (𝜑 → 𝐴 ∈ 𝑤)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2109   ≠ wne 2926  ∀wral 3045  ∃wrex 3054   ∪ cun 3915   ⊆ wss 3917  ∅c0 4299  {csn 4592  {cpr 4594  ∪ cuni 4874

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

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 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-ne 2927  df-ral 3046  df-rex 3055  df-v 3452  df-dif 3920  df-un 3922  df-ss 3934  df-nul 4300  df-sn 4593  df-pr 4595  df-uni 4875

This theorem is referenced by:  mnuprdlem4  44271