Theorem mnuprdlem1 43333

Description: Lemma for mnuprd 43337. (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 2819	. . . . 5 ⊢ (𝑖 = ∅ → (𝑖 ∈ 𝑢 ↔ ∅ ∈ 𝑢))
2	1	anbi1d 628	. . . 4 ⊢ (𝑖 = ∅ → ((𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
3	2	rexbidv 3176	. . 3 ⊢ (𝑖 = ∅ → (∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
4		mnuprdlem1.8	. . 3 ⊢ (𝜑 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
5		0ex 5306	. . . . 5 ⊢ ∅ ∈ V
6	5	prid1 4765	. . . 4 ⊢ ∅ ∈ {∅, {∅}}
7	6	a1i 11	. . 3 ⊢ (𝜑 → ∅ ∈ {∅, {∅}})
8	3, 4, 7	rspcdva 3612	. 2 ⊢ (𝜑 → ∃𝑢 ∈ 𝐹 (∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
9		mnuprdlem1.3	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
10	9	adantr 479	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑈)
11		simprl 767	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 ∈ 𝐹)
12		simpr 483	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ∅ ∈ 𝑎)
13		0nep0 5355	. . . . . . . . . . . . 13 ⊢ ∅ ≠ {∅}
14	13	a1i 11	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {∅})
15		mnuprdlem1.4	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
16	15	snn0d 4778	. . . . . . . . . . . . 13 ⊢ (𝜑 → {𝐵} ≠ ∅)
17	16	necomd 2994	. . . . . . . . . . . 12 ⊢ (𝜑 → ∅ ≠ {𝐵})
18	14, 17	nelprd 4658	. . . . . . . . . . 11 ⊢ (𝜑 → ¬ ∅ ∈ {{∅}, {𝐵}})
19	18	adantr 479	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ ∅ ∈ {{∅}, {𝐵}})
20	12, 19	elnelneqd 43256	. . . . . . . . 9 ⊢ ((𝜑 ∧ ∅ ∈ 𝑎) → ¬ 𝑎 = {{∅}, {𝐵}})
21	20	adantrr 713	. . . . . . . 8 ⊢ ((𝜑 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)) → ¬ 𝑎 = {{∅}, {𝐵}})
22	21	adantrl 712	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ¬ 𝑎 = {{∅}, {𝐵}})
23		elpri 4649	. . . . . . . . . 10 ⊢ (𝑎 ∈ {{∅, {𝐴}}, {{∅}, {𝐵}}} → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
24		mnuprdlem1.1	. . . . . . . . . 10 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
25	23, 24	eleq2s 2849	. . . . . . . . 9 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {∅, {𝐴}} ∨ 𝑎 = {{∅}, {𝐵}}))
26	25	orcomd 867	. . . . . . . 8 ⊢ (𝑎 ∈ 𝐹 → (𝑎 = {{∅}, {𝐵}} ∨ 𝑎 = {∅, {𝐴}}))
27	26	ord 860	. . . . . . 7 ⊢ (𝑎 ∈ 𝐹 → (¬ 𝑎 = {{∅}, {𝐵}} → 𝑎 = {∅, {𝐴}}))
28	11, 22, 27	sylc 65	. . . . . 6 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝑎 = {∅, {𝐴}})
29	28	unieqd 4921	. . . . 5 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = ∪ {∅, {𝐴}})
30		snex 5430	. . . . . . 7 ⊢ {𝐴} ∈ V
31	5, 30	unipr 4925	. . . . . 6 ⊢ ∪ {∅, {𝐴}} = (∅ ∪ {𝐴})
32		uncom 4152	. . . . . 6 ⊢ (∅ ∪ {𝐴}) = ({𝐴} ∪ ∅)
33		un0 4389	. . . . . 6 ⊢ ({𝐴} ∪ ∅) = {𝐴}
34	31, 32, 33	3eqtri 2762	. . . . 5 ⊢ ∪ {∅, {𝐴}} = {𝐴}
35	29, 34	eqtrdi 2786	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 = {𝐴})
36		simprrr 778	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → ∪ 𝑎 ⊆ 𝑤)
37	35, 36	eqsstrrd 4020	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → {𝐴} ⊆ 𝑤)
38		snssg 4786	. . . 4 ⊢ (𝐴 ∈ 𝑈 → (𝐴 ∈ 𝑤 ↔ {𝐴} ⊆ 𝑤))
39	38	biimprd 247	. . 3 ⊢ (𝐴 ∈ 𝑈 → ({𝐴} ⊆ 𝑤 → 𝐴 ∈ 𝑤))
40	10, 37, 39	sylc 65	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝐹 ∧ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤))) → 𝐴 ∈ 𝑤)
41		eleq2w 2815	. . 3 ⊢ (𝑢 = 𝑎 → (∅ ∈ 𝑢 ↔ ∅ ∈ 𝑎))
42		unieq 4918	. . . 4 ⊢ (𝑢 = 𝑎 → ∪ 𝑢 = ∪ 𝑎)
43	42	sseq1d 4012	. . 3 ⊢ (𝑢 = 𝑎 → (∪ 𝑢 ⊆ 𝑤 ↔ ∪ 𝑎 ⊆ 𝑤))
44	41, 43	anbi12d 629	. 2 ⊢ (𝑢 = 𝑎 → ((∅ ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤) ↔ (∅ ∈ 𝑎 ∧ ∪ 𝑎 ⊆ 𝑤)))
45	8, 40, 44	rexlimddvcbvw 43260	1 ⊢ (𝜑 → 𝐴 ∈ 𝑤)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 394   ∨ wo 843   = wceq 1539   ∈ wcel 2104   ≠ wne 2938  ∀wral 3059  ∃wrex 3068   ∪ cun 3945   ⊆ wss 3947  ∅c0 4321  {csn 4627  {cpr 4629  ∪ cuni 4907

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-sn 4628  df-pr 4630  df-uni 4908

This theorem is referenced by:  mnuprdlem4  43336