Theorem rr-grothshort

Description: A shorter equivalent of ax-groth than rr-groth using a few more simple defined symbols. (Contributed by Rohan Ridenour, 8-Oct-2024)

	Ref	Expression
Assertion	rr-grothshort	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )

Proof

Step	Hyp	Ref	Expression
1		gruex	⊢ ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦
2	1	ax-gen	⊢ ∀ 𝑥 ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦
3		rr-grothshortbi	⊢ ( ∀ 𝑥 ∃ 𝑦 ∈ Univ 𝑥 ∈ 𝑦 ↔ ∀ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) ) )
4	2 3	mpbi	⊢ ∀ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )
5	4	spi	⊢ ∃ 𝑦 ( 𝑥 ∈ 𝑦 ∧ ∀ 𝑧 ∈ 𝑦 ∀ 𝑓 ∈ 𝒫 𝑦 ∃ 𝑤 ∈ 𝑦 ( 𝒫 𝑧 ⊆ ( 𝑦 ∩ 𝑤 ) ∧ ( 𝑧 ∩ ∪ 𝑓 ) ⊆ ∪ ( 𝑓 ∩ 𝒫 𝒫 𝑤 ) ) )