Theorem mnuprdlem4 40983

Description: Lemma for mnuprd 40984. 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 40973	. . . . . 6 ⊢ (𝜑 → ∅ ∈ 𝑈)
5	1, 2, 4	mnusnd 40976	. . . . 5 ⊢ (𝜑 → {∅} ∈ 𝑈)
6		0ss 4304	. . . . 5 ⊢ ∅ ⊆ {∅}
7		ssid 3937	. . . . 5 ⊢ {∅} ⊆ {∅}
8	1, 2, 5, 6, 7	mnuprss2d 40978	. . . 4 ⊢ (𝜑 → {∅, {∅}} ∈ 𝑈)
9		mnuprdlem4.2	. . . . 5 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
10	1, 2, 3	mnusnd 40976	. . . . . . 7 ⊢ (𝜑 → {𝐴} ∈ 𝑈)
11		0ss 4304	. . . . . . 7 ⊢ ∅ ⊆ {𝐴}
12		ssid 3937	. . . . . . 7 ⊢ {𝐴} ⊆ {𝐴}
13	1, 2, 10, 11, 12	mnuprss2d 40978	. . . . . 6 ⊢ (𝜑 → {∅, {𝐴}} ∈ 𝑈)
14		mnuprdlem4.5	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
15		0ss 4304	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
16		ssid 3937	. . . . . . . 8 ⊢ 𝐵 ⊆ 𝐵
17	1, 2, 14, 15, 16	mnuprss2d 40978	. . . . . . 7 ⊢ (𝜑 → {∅, 𝐵} ∈ 𝑈)
18		snsspr1 4707	. . . . . . 7 ⊢ {∅} ⊆ {∅, 𝐵}
19		snsspr2 4708	. . . . . . 7 ⊢ {𝐵} ⊆ {∅, 𝐵}
20	1, 2, 17, 18, 19	mnuprss2d 40978	. . . . . 6 ⊢ (𝜑 → {{∅}, {𝐵}} ∈ 𝑈)
21	13, 20	prssd 4715	. . . . 5 ⊢ (𝜑 → {{∅, {𝐴}}, {{∅}, {𝐵}}} ⊆ 𝑈)
22	9, 21	eqsstrid 3963	. . . 4 ⊢ (𝜑 → 𝐹 ⊆ 𝑈)
23	1, 2, 8, 22	mnuop3d 40979	. . 3 ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
24		simprl 770	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝑤 ∈ 𝑈)
25		eleq2w 2873	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤))
26		eleq2w 2873	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐵 ∈ 𝑎 ↔ 𝐵 ∈ 𝑤))
27	25, 26	anbi12d 633	. . . . 5 ⊢ (𝑎 = 𝑤 → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
28	27	adantl 485	. . . 4 ⊢ (((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑎 = 𝑤) → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
29	3	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑈)
30	14	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑈)
31		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑖𝜑
32		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑖 𝑤 ∈ 𝑈
33		nfra1 3183	. . . . . . . . . 10 ⊢ Ⅎ𝑖∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
34	32, 33	nfan 1900	. . . . . . . . 9 ⊢ Ⅎ𝑖(𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
35	31, 34	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
36	9, 35	mnuprdlem3 40982	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
37		ralim 3130	. . . . . . . 8 ⊢ (∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
38	37	ad2antll 728	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
39	36, 38	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
40	9, 29, 30, 39	mnuprdlem1 40980	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑤)
41		mnuprdlem4.6	. . . . . . 7 ⊢ (𝜑 → ¬ 𝐴 = ∅)
42	41	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ¬ 𝐴 = ∅)
43	9, 30, 42, 39	mnuprdlem2 40981	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑤)
44	40, 43	jca 515	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤))
45	24, 28, 44	rspcedvd 3574	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
46	23, 45	rexlimddv 3250	. 2 ⊢ (𝜑 → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
47	2	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑈 ∈ 𝑀)
48		simprl 770	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑎 ∈ 𝑈)
49		simprrl 780	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐴 ∈ 𝑎)
50		simprrr 781	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐵 ∈ 𝑎)
51	49, 50	prssd 4715	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ⊆ 𝑎)
52	1, 47, 48, 51	mnussd 40971	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ∈ 𝑈)
53	46, 52	rexlimddv 3250	1 ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399  ∀wal 1536   = wceq 1538   ∈ wcel 2111  {cab 2776  ∀wral 3106  ∃wrex 3107   ⊆ wss 3881  ∅c0 4243  𝒫 cpw 4497  {csn 4525  {cpr 4527  ∪ cuni 4800

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526  df-pr 4528  df-uni 4801

This theorem is referenced by:  mnuprd  40984