Theorem mnuprdlem4 44812

Description: Lemma for mnuprd 44813. 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 44802	. . . . . 6 ⊢ (𝜑 → ∅ ∈ 𝑈)
5	1, 2, 4	mnusnd 44805	. . . . 5 ⊢ (𝜑 → {∅} ∈ 𝑈)
6		0ss 4351	. . . . 5 ⊢ ∅ ⊆ {∅}
7		ssid 3956	. . . . 5 ⊢ {∅} ⊆ {∅}
8	1, 2, 5, 6, 7	mnuprss2d 44807	. . . 4 ⊢ (𝜑 → {∅, {∅}} ∈ 𝑈)
9		mnuprdlem4.2	. . . . 5 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
10	1, 2, 3	mnusnd 44805	. . . . . . 7 ⊢ (𝜑 → {𝐴} ∈ 𝑈)
11		0ss 4351	. . . . . . 7 ⊢ ∅ ⊆ {𝐴}
12		ssid 3956	. . . . . . 7 ⊢ {𝐴} ⊆ {𝐴}
13	1, 2, 10, 11, 12	mnuprss2d 44807	. . . . . 6 ⊢ (𝜑 → {∅, {𝐴}} ∈ 𝑈)
14		mnuprdlem4.5	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
15		0ss 4351	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
16		ssid 3956	. . . . . . . 8 ⊢ 𝐵 ⊆ 𝐵
17	1, 2, 14, 15, 16	mnuprss2d 44807	. . . . . . 7 ⊢ (𝜑 → {∅, 𝐵} ∈ 𝑈)
18		snsspr1 4769	. . . . . . 7 ⊢ {∅} ⊆ {∅, 𝐵}
19		snsspr2 4770	. . . . . . 7 ⊢ {𝐵} ⊆ {∅, 𝐵}
20	1, 2, 17, 18, 19	mnuprss2d 44807	. . . . . 6 ⊢ (𝜑 → {{∅}, {𝐵}} ∈ 𝑈)
21	13, 20	prssd 4777	. . . . 5 ⊢ (𝜑 → {{∅, {𝐴}}, {{∅}, {𝐵}}} ⊆ 𝑈)
22	9, 21	eqsstrid 3972	. . . 4 ⊢ (𝜑 → 𝐹 ⊆ 𝑈)
23	1, 2, 8, 22	mnuop3d 44808	. . 3 ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
24		simprl 780	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝑤 ∈ 𝑈)
25		eleq2w 2845	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤))
26		eleq2w 2845	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐵 ∈ 𝑎 ↔ 𝐵 ∈ 𝑤))
27	25, 26	anbi12d 641	. . . . 5 ⊢ (𝑎 = 𝑤 → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
28	27	adantl 485	. . . 4 ⊢ (((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑎 = 𝑤) → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
29	3	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑈)
30	14	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑈)
31		nfv 1933	. . . . . . . . 9 ⊢ Ⅎ𝑖𝜑
32		nfv 1933	. . . . . . . . . 10 ⊢ Ⅎ𝑖 𝑤 ∈ 𝑈
33		nfra1 3285	. . . . . . . . . 10 ⊢ Ⅎ𝑖∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
34	32, 33	nfan 1918	. . . . . . . . 9 ⊢ Ⅎ𝑖(𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
35	31, 34	nfan 1918	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
36	9, 35	mnuprdlem3 44811	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
37		ralim 3101	. . . . . . . 8 ⊢ (∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
38	37	ad2antll 739	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
39	36, 38	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
40	9, 29, 30, 39	mnuprdlem1 44809	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑤)
41		mnuprdlem4.6	. . . . . . 7 ⊢ (𝜑 → ¬ 𝐴 = ∅)
42	41	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ¬ 𝐴 = ∅)
43	9, 30, 42, 39	mnuprdlem2 44810	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑤)
44	40, 43	jca 519	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤))
45	24, 28, 44	rspcedvd 3582	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
46	23, 45	rexlimddv 3168	. 2 ⊢ (𝜑 → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
47	2	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑈 ∈ 𝑀)
48		simprl 780	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑎 ∈ 𝑈)
49		simprrl 790	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐴 ∈ 𝑎)
50		simprrr 791	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐵 ∈ 𝑎)
51	49, 50	prssd 4777	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ⊆ 𝑎)
52	1, 47, 48, 51	mnussd 44800	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ∈ 𝑈)
53	46, 52	rexlimddv 3168	1 ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399  ∀wal 1557   = wceq 1559   ∈ wcel 2141  {cab 2739  ∀wral 3075  ∃wrex 3085   ⊆ wss 3902  ∅c0 4283  𝒫 cpw 4552  {csn 4579  {cpr 4581  ∪ cuni 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-pw 4554  df-sn 4580  df-pr 4582  df-uni 4863

This theorem is referenced by:  mnuprd  44813