Theorem mnuprdlem4

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

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

Proof

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