Theorem mnuop3d

Description: Third operation of a minimal universe. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnuop3d.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
	mnuop3d.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
	mnuop3d.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	mnuop3d.4	⊢ ( 𝜑 → 𝐹 ⊆ 𝑈 )
Assertion	mnuop3d	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑈 ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		mnuop3d.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnuop3d.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3		mnuop3d.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
4		mnuop3d.4	⊢ ( 𝜑 → 𝐹 ⊆ 𝑈 )
5	2 4	sselpwd	⊢ ( 𝜑 → 𝐹 ∈ 𝒫 𝑈 )
6	1 2 3 5	mnuop23d	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
7	4	sseld	⊢ ( 𝜑 → ( 𝑣 ∈ 𝐹 → 𝑣 ∈ 𝑈 ) )
8	7	adantrd	⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐹 ∧ 𝑖 ∈ 𝑣 ) → 𝑣 ∈ 𝑈 ) )
9		pm3.22	⊢ ( ( 𝑣 ∈ 𝐹 ∧ 𝑖 ∈ 𝑣 ) → ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) )
10	8 9	jca2	⊢ ( 𝜑 → ( ( 𝑣 ∈ 𝐹 ∧ 𝑖 ∈ 𝑣 ) → ( 𝑣 ∈ 𝑈 ∧ ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) ) ) )
11	10	reximdv2	⊢ ( 𝜑 → ( ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) ) )
12	11	imim1d	⊢ ( 𝜑 → ( ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) → ( ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
13	12	ralimdv	⊢ ( 𝜑 → ( ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) → ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
14	13	adantld	⊢ ( 𝜑 → ( ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) → ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
15	14	reximdv	⊢ ( 𝜑 → ( ∃ 𝑤 ∈ 𝑈 ( 𝒫 𝐴 ⊆ 𝑤 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝑈 ( 𝑖 ∈ 𝑣 ∧ 𝑣 ∈ 𝐹 ) → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) → ∃ 𝑤 ∈ 𝑈 ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) )
16	6 15	mpd	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑈 ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ 𝐹 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ 𝐹 ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )