Theorem mnuprdlem4 40660

Description: Lemma for mnuprd 40661. 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 40650	. . . . . 6 ⊢ (𝜑 → ∅ ∈ 𝑈)
5	1, 2, 4	mnusnd 40653	. . . . 5 ⊢ (𝜑 → {∅} ∈ 𝑈)
6		0ss 4350	. . . . 5 ⊢ ∅ ⊆ {∅}
7		ssid 3989	. . . . 5 ⊢ {∅} ⊆ {∅}
8	1, 2, 5, 6, 7	mnuprss2d 40655	. . . 4 ⊢ (𝜑 → {∅, {∅}} ∈ 𝑈)
9		mnuprdlem4.2	. . . . 5 ⊢ 𝐹 = {{∅, {𝐴}}, {{∅}, {𝐵}}}
10	1, 2, 3	mnusnd 40653	. . . . . . 7 ⊢ (𝜑 → {𝐴} ∈ 𝑈)
11		0ss 4350	. . . . . . 7 ⊢ ∅ ⊆ {𝐴}
12		ssid 3989	. . . . . . 7 ⊢ {𝐴} ⊆ {𝐴}
13	1, 2, 10, 11, 12	mnuprss2d 40655	. . . . . 6 ⊢ (𝜑 → {∅, {𝐴}} ∈ 𝑈)
14		mnuprdlem4.5	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝑈)
15		0ss 4350	. . . . . . . 8 ⊢ ∅ ⊆ 𝐵
16		ssid 3989	. . . . . . . 8 ⊢ 𝐵 ⊆ 𝐵
17	1, 2, 14, 15, 16	mnuprss2d 40655	. . . . . . 7 ⊢ (𝜑 → {∅, 𝐵} ∈ 𝑈)
18		snsspr1 4747	. . . . . . 7 ⊢ {∅} ⊆ {∅, 𝐵}
19		snsspr2 4748	. . . . . . 7 ⊢ {𝐵} ⊆ {∅, 𝐵}
20	1, 2, 17, 18, 19	mnuprss2d 40655	. . . . . 6 ⊢ (𝜑 → {{∅}, {𝐵}} ∈ 𝑈)
21	13, 20	prssd 4755	. . . . 5 ⊢ (𝜑 → {{∅, {𝐴}}, {{∅}, {𝐵}}} ⊆ 𝑈)
22	9, 21	eqsstrid 4015	. . . 4 ⊢ (𝜑 → 𝐹 ⊆ 𝑈)
23	1, 2, 8, 22	mnuop3d 40656	. . 3 ⊢ (𝜑 → ∃𝑤 ∈ 𝑈 ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
24		simprl 769	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝑤 ∈ 𝑈)
25		eleq2w 2896	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑤))
26		eleq2w 2896	. . . . . 6 ⊢ (𝑎 = 𝑤 → (𝐵 ∈ 𝑎 ↔ 𝐵 ∈ 𝑤))
27	25, 26	anbi12d 632	. . . . 5 ⊢ (𝑎 = 𝑤 → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
28	27	adantl 484	. . . 4 ⊢ (((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) ∧ 𝑎 = 𝑤) → ((𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎) ↔ (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤)))
29	3	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑈)
30	14	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑈)
31		nfv 1915	. . . . . . . . 9 ⊢ Ⅎ𝑖𝜑
32		nfv 1915	. . . . . . . . . 10 ⊢ Ⅎ𝑖 𝑤 ∈ 𝑈
33		nfra1 3219	. . . . . . . . . 10 ⊢ Ⅎ𝑖∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
34	32, 33	nfan 1900	. . . . . . . . 9 ⊢ Ⅎ𝑖(𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
35	31, 34	nfan 1900	. . . . . . . 8 ⊢ Ⅎ𝑖(𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))))
36	9, 35	mnuprdlem3 40659	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣)
37		ralim 3162	. . . . . . . 8 ⊢ (∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
38	37	ad2antll 727	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (∀𝑖 ∈ {∅, {∅}}∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))
39	36, 38	mpd 15	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∀𝑖 ∈ {∅, {∅}}∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤))
40	9, 29, 30, 39	mnuprdlem1 40657	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐴 ∈ 𝑤)
41		mnuprdlem4.6	. . . . . . 7 ⊢ (𝜑 → ¬ 𝐴 = ∅)
42	41	adantr 483	. . . . . 6 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ¬ 𝐴 = ∅)
43	9, 30, 42, 39	mnuprdlem2 40658	. . . . 5 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → 𝐵 ∈ 𝑤)
44	40, 43	jca 514	. . . 4 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → (𝐴 ∈ 𝑤 ∧ 𝐵 ∈ 𝑤))
45	24, 28, 44	rspcedvd 3626	. . 3 ⊢ ((𝜑 ∧ (𝑤 ∈ 𝑈 ∧ ∀𝑖 ∈ {∅, {∅}} (∃𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃𝑢 ∈ 𝐹 (𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤)))) → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
46	23, 45	rexlimddv 3291	. 2 ⊢ (𝜑 → ∃𝑎 ∈ 𝑈 (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))
47	2	adantr 483	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑈 ∈ 𝑀)
48		simprl 769	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝑎 ∈ 𝑈)
49		simprrl 779	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐴 ∈ 𝑎)
50		simprrr 780	. . . 4 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → 𝐵 ∈ 𝑎)
51	49, 50	prssd 4755	. . 3 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ⊆ 𝑎)
52	1, 47, 48, 51	mnussd 40648	. 2 ⊢ ((𝜑 ∧ (𝑎 ∈ 𝑈 ∧ (𝐴 ∈ 𝑎 ∧ 𝐵 ∈ 𝑎))) → {𝐴, 𝐵} ∈ 𝑈)
53	46, 52	rexlimddv 3291	1 ⊢ (𝜑 → {𝐴, 𝐵} ∈ 𝑈)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398  ∀wal 1535   = wceq 1537   ∈ wcel 2114  {cab 2799  ∀wral 3138  ∃wrex 3139   ⊆ wss 3936  ∅c0 4291  𝒫 cpw 4539  {csn 4567  {cpr 4569  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-pw 4541  df-sn 4568  df-pr 4570  df-uni 4839

This theorem is referenced by:  mnuprd  40661