Theorem mnuprdlem4 41782

Description: Lemma for mnuprd 41783. General case. (Contributed by Rohan Ridenour, 13-Aug-2023.)

Hypotheses

Ref	Expression
mnuprdlem4.1	⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}
mnuprdlem4.2	⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
mnuprdlem4.3	⊢ (𝜑 → 𝑈 ∈ 𝑀)
mnuprdlem4.4	⊢ (𝜑 → 𝐴 ∈ 𝑈)
mnuprdlem4.5	⊢ (𝜑 → 𝐵 ∈ 𝑈)
mnuprdlem4.6	⊢ (𝜑 → ¬ 𝐴 = ∅)

Assertion

Ref	Expression
mnuprdlem4	⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)

Distinct variable groups:   𝑈,𝑘,𝑚,𝑛,𝑞,𝑝,𝑙   𝑈,𝑟,𝑘,𝑚,𝑛,𝑝,𝑙

Allowed substitution hints:   𝜑(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝐴(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝐵(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝐹(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)   𝑀(𝑘,𝑚,𝑛,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem mnuprdlem4

Dummy variables 𝑣 𝑤 𝑎 𝑖 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		mnuprdlem4.1	. . . 4 ⊢ 𝑀 = {𝑘 ∣ ∀𝑙 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑘 ∧ ∀𝑚∃𝑛 ∈ 𝑘 (𝒫 𝑙 ⊆ 𝑛 ∧ ∀𝑝 ∈ 𝑙 (∃𝑞 ∈ 𝑘 (𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚) → ∃𝑟 ∈ 𝑚 (𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛))))}
2		mnuprdlem4.3	. . . 4 ⊢ (𝜑 → 𝑈 ∈ 𝑀)
3		mnuprdlem4.4	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ 𝑈)
4	1, 2, 3	mnu0eld 41772	. . . . . 6 ⊢ (𝜑 → ∅ ∈ 𝑈)
5	1, 2, 4	mnusnd 41775	. . . . 5 ⊢ (𝜑 → {∅} ∈ 𝑈)
6		0ss 4327	. . . . 5 ⊢ ∅ ⊆ {∅}
7		ssid 3939	. . . . 5 ⊢ {∅} ⊆ {∅}
8	1, 2, 5, 6, 7	mnuprss2d 41777	. . . 4 ⊢ (𝜑 → {∅, {∅}} ∈ 𝑈)
9		mnuprdlem4.2	. . . . 5 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
10	1, 2, 3	mnusnd 41775	. . . . . . 7 ⊢ (𝜑 → {𝐴} ∈ 𝑈)
11		0ss 4327	. . . . . . 7 ⊢ ∅ ⊆ {𝐴}
12		ssid 3939	. . . . . . 7 ⊢ {𝐴} ⊆ {𝐴}
13	1, 2, 10, 11, 12	mnuprss2d 41777	. . . . . 6 ⊢ (𝜑 → {∅, {𝐴}} ∈ 𝑈)
14		mnuprdlem4.5	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
15		0ss 4327	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
16		ssid 3939	. . . . . . . 8 ⊢ 𝐵 ⊆ 𝐵
17	1, 2, 14, 15, 16	mnuprss2d 41777	. . . . . . 7 ⊢ (𝜑 → {∅, 𝐵} ∈ 𝑈)
18		snsspr1 4744	. . . . . . 7 ⊢ {∅} ⊆ {∅, 𝐵}
19		snsspr2 4745	. . . . . . 7 ⊢ {𝐵} ⊆ {∅, 𝐵}
20	1, 2, 17, 18, 19	mnuprss2d 41777	. . . . . 6 ⊢ (𝜑 → {{∅}, {𝐵}} ∈ 𝑈)
21	13, 20	prssd 4752	. . . . 5 ⊢ (𝜑 → {{∅, {𝐴}}, {{∅}, {𝐵}}} ⊆ 𝑈)
22	9, 21	eqsstrid 3965	. . . 4 ⊢ (𝜑 → 𝐹 ⊆ 𝑈)
23	1, 2, 8, 22	mnuop3d 41778	. . 3 ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
24		simprl 767	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝑤 ∈ 𝑈)
25		eleq2w 2822	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤))
26		eleq2w 2822	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐵 ∈ 𝑎 ↔ 𝐵 ∈ 𝑤))
27	25, 26	anbi12d 630	. . . . 5 ⊢ (𝑎 = 𝑤 → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
28	27	adantl 481	. . . 4 ⊢ (((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑎 = 𝑤) → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
29	3	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑈)
30	14	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑈)
31		nfv 1918	. . . . . . . . 9 ⊢ Ⅎ𝑖𝜑
32		nfv 1918	. . . . . . . . . 10 ⊢ Ⅎ𝑖 𝑤 ∈ 𝑈
33		nfra1 3142	. . . . . . . . . 10 ⊢ Ⅎ𝑖∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
34	32, 33	nfan 1903	. . . . . . . . 9 ⊢ Ⅎ𝑖(𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
35	31, 34	nfan 1903	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
36	9, 35	mnuprdlem3 41781	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
37		ralim 3082	. . . . . . . 8 ⊢ (∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
38	37	ad2antll 725	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
39	36, 38	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
40	9, 29, 30, 39	mnuprdlem1 41779	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑤)
41		mnuprdlem4.6	. . . . . . 7 ⊢ (𝜑 → ¬ 𝐴 = ∅)
42	41	adantr 480	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ¬ 𝐴 = ∅)
43	9, 30, 42, 39	mnuprdlem2 41780	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑤)
44	40, 43	jca 511	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤))
45	24, 28, 44	rspcedvd 3555	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
46	23, 45	rexlimddv 3219	. 2 ⊢ (𝜑 → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
47	2	adantr 480	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑈 ∈ 𝑀)
48		simprl 767	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑎 ∈ 𝑈)
49		simprrl 777	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐴 ∈ 𝑎)
50		simprrr 778	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐵 ∈ 𝑎)
51	49, 50	prssd 4752	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ⊆ 𝑎)
52	1, 47, 48, 51	mnussd 41770	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ∈ 𝑈)
53	46, 52	rexlimddv 3219	1 ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537   = wceq 1539   ∈ wcel 2108  {cab 2715  ∀wral 3063  ∃wrex 3064   ⊆ wss 3883  ∅c0 4253  𝒫 cpw 4530  {csn 4558  {cpr 4560  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-pw 4532  df-sn 4559  df-pr 4561  df-uni 4837

This theorem is referenced by:  mnuprd  41783