Theorem mnuprdlem4 45018

Description: Lemma for mnuprd 45019. 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 45008	. . . . . 6 ⊢ (𝜑 → ∅ ∈ 𝑈)
5	1, 2, 4	mnusnd 45011	. . . . 5 ⊢ (𝜑 → {∅} ∈ 𝑈)
6		0ss 4357	. . . . 5 ⊢ ∅ ⊆ {∅}
7		ssid 3960	. . . . 5 ⊢ {∅} ⊆ {∅}
8	1, 2, 5, 6, 7	mnuprss2d 45013	. . . 4 ⊢ (𝜑 → {∅, {∅}} ∈ 𝑈)
9		mnuprdlem4.2	. . . . 5 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
10	1, 2, 3	mnusnd 45011	. . . . . . 7 ⊢ (𝜑 → {𝐴} ∈ 𝑈)
11		0ss 4357	. . . . . . 7 ⊢ ∅ ⊆ {𝐴}
12		ssid 3960	. . . . . . 7 ⊢ {𝐴} ⊆ {𝐴}
13	1, 2, 10, 11, 12	mnuprss2d 45013	. . . . . 6 ⊢ (𝜑 → {∅, {𝐴}} ∈ 𝑈)
14		mnuprdlem4.5	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
15		0ss 4357	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
16		ssid 3960	. . . . . . . 8 ⊢ 𝐵 ⊆ 𝐵
17	1, 2, 14, 15, 16	mnuprss2d 45013	. . . . . . 7 ⊢ (𝜑 → {∅, 𝐵} ∈ 𝑈)
18		snsspr1 4782	. . . . . . 7 ⊢ {∅} ⊆ {∅, 𝐵}
19		snsspr2 4783	. . . . . . 7 ⊢ {𝐵} ⊆ {∅, 𝐵}
20	1, 2, 17, 18, 19	mnuprss2d 45013	. . . . . 6 ⊢ (𝜑 → {{∅}, {𝐵}} ∈ 𝑈)
21	13, 20	prssd 4790	. . . . 5 ⊢ (𝜑 → {{∅, {𝐴}}, {{∅}, {𝐵}}} ⊆ 𝑈)
22	9, 21	eqsstrid 3976	. . . 4 ⊢ (𝜑 → 𝐹 ⊆ 𝑈)
23	1, 2, 8, 22	mnuop3d 45014	. . 3 ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
24		simprl 783	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝑤 ∈ 𝑈)
25		eleq2w 2849	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤))
26		eleq2w 2849	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐵 ∈ 𝑎 ↔ 𝐵 ∈ 𝑤))
27	25, 26	anbi12d 644	. . . . 5 ⊢ (𝑎 = 𝑤 → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
28	27	adantl 487	. . . 4 ⊢ (((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑎 = 𝑤) → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
29	3	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑈)
30	14	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑈)
31		nfv 1947	. . . . . . . . 9 ⊢ Ⅎ𝑖𝜑
32		nfv 1947	. . . . . . . . . 10 ⊢ Ⅎ𝑖 𝑤 ∈ 𝑈
33		nfra1 3291	. . . . . . . . . 10 ⊢ Ⅎ𝑖∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
34	32, 33	nfan 1932	. . . . . . . . 9 ⊢ Ⅎ𝑖(𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
35	31, 34	nfan 1932	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
36	9, 35	mnuprdlem3 45017	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
37		ralim 3107	. . . . . . . 8 ⊢ (∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
38	37	ad2antll 742	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
39	36, 38	mpd 16	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
40	9, 29, 30, 39	mnuprdlem1 45015	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑤)
41		mnuprdlem4.6	. . . . . . 7 ⊢ (𝜑 → ¬ 𝐴 = ∅)
42	41	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ¬ 𝐴 = ∅)
43	9, 30, 42, 39	mnuprdlem2 45016	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑤)
44	40, 43	jca 521	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤))
45	24, 28, 44	rspcedvd 3585	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
46	23, 45	rexlimddv 3174	. 2 ⊢ (𝜑 → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
47	2	adantr 486	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑈 ∈ 𝑀)
48		simprl 783	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑎 ∈ 𝑈)
49		simprrl 793	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐴 ∈ 𝑎)
50		simprrr 794	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐵 ∈ 𝑎)
51	49, 50	prssd 4790	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ⊆ 𝑎)
52	1, 47, 48, 51	mnussd 45006	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ∈ 𝑈)
53	46, 52	rexlimddv 3174	1 ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570   ∈ wcel 2146  {cab 2743  ∀wral 3081  ∃wrex 3091   ⊆ wss 3906  ∅c0 4286  𝒫 cpw 4564  {csn 4591  {cpr 4593  ∪ cuni 4874

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-pw 4566  df-sn 4592  df-pr 4594  df-uni 4875

This theorem is used by:  mnuprd  45019