Theorem clrellem

Description: When the property ps holds for a relation substituted for x , then the closure on that property is a relation if the base set is a relation. (Contributed by RP, 30-Jul-2020)

	Ref	Expression
Hypotheses	clrellem.y	⊢ ( 𝜑 → 𝑌 ∈ V )
	clrellem.rel	⊢ ( 𝜑 → Rel 𝑋 )
	clrellem.sub	⊢ ( 𝑥 = ◡ ◡ 𝑌 → ( 𝜓 ↔ 𝜒 ) )
	clrellem.sup	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
	clrellem.maj	⊢ ( 𝜑 → 𝜒 )
Assertion	clrellem	⊢ ( 𝜑 → Rel ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } )

Proof

Step	Hyp	Ref	Expression
1		clrellem.y	⊢ ( 𝜑 → 𝑌 ∈ V )
2		clrellem.rel	⊢ ( 𝜑 → Rel 𝑋 )
3		clrellem.sub	⊢ ( 𝑥 = ◡ ◡ 𝑌 → ( 𝜓 ↔ 𝜒 ) )
4		clrellem.sup	⊢ ( 𝜑 → 𝑋 ⊆ 𝑌 )
5		clrellem.maj	⊢ ( 𝜑 → 𝜒 )
6		cnvexg	⊢ ( 𝑌 ∈ V → ◡ 𝑌 ∈ V )
7		cnvexg	⊢ ( ◡ 𝑌 ∈ V → ◡ ◡ 𝑌 ∈ V )
8	1 6 7	3syl	⊢ ( 𝜑 → ◡ ◡ 𝑌 ∈ V )
9		dfrel2	⊢ ( Rel 𝑋 ↔ ◡ ◡ 𝑋 = 𝑋 )
10	2 9	sylib	⊢ ( 𝜑 → ◡ ◡ 𝑋 = 𝑋 )
11		cnvss	⊢ ( 𝑋 ⊆ 𝑌 → ◡ 𝑋 ⊆ ◡ 𝑌 )
12		cnvss	⊢ ( ◡ 𝑋 ⊆ ◡ 𝑌 → ◡ ◡ 𝑋 ⊆ ◡ ◡ 𝑌 )
13	4 11 12	3syl	⊢ ( 𝜑 → ◡ ◡ 𝑋 ⊆ ◡ ◡ 𝑌 )
14	10 13	eqsstrrd	⊢ ( 𝜑 → 𝑋 ⊆ ◡ ◡ 𝑌 )
15		relcnv	⊢ Rel ◡ ◡ 𝑌
16	15	a1i	⊢ ( 𝜑 → Rel ◡ ◡ 𝑌 )
17	14 5 16	jca31	⊢ ( 𝜑 → ( ( 𝑋 ⊆ ◡ ◡ 𝑌 ∧ 𝜒 ) ∧ Rel ◡ ◡ 𝑌 ) )
18	3	cleq2lem	⊢ ( 𝑥 = ◡ ◡ 𝑌 → ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ↔ ( 𝑋 ⊆ ◡ ◡ 𝑌 ∧ 𝜒 ) ) )
19		releq	⊢ ( 𝑥 = ◡ ◡ 𝑌 → ( Rel 𝑥 ↔ Rel ◡ ◡ 𝑌 ) )
20	18 19	anbi12d	⊢ ( 𝑥 = ◡ ◡ 𝑌 → ( ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ∧ Rel 𝑥 ) ↔ ( ( 𝑋 ⊆ ◡ ◡ 𝑌 ∧ 𝜒 ) ∧ Rel ◡ ◡ 𝑌 ) ) )
21	8 17 20	spcedv	⊢ ( 𝜑 → ∃ 𝑥 ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ∧ Rel 𝑥 ) )
22		releq	⊢ ( 𝑦 = 𝑥 → ( Rel 𝑦 ↔ Rel 𝑥 ) )
23	22	rexab2	⊢ ( ∃ 𝑦 ∈ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } Rel 𝑦 ↔ ∃ 𝑥 ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ∧ Rel 𝑥 ) )
24	23	biimpri	⊢ ( ∃ 𝑥 ( ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) ∧ Rel 𝑥 ) → ∃ 𝑦 ∈ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } Rel 𝑦 )
25		relint	⊢ ( ∃ 𝑦 ∈ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } Rel 𝑦 → Rel ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } )
26	21 24 25	3syl	⊢ ( 𝜑 → Rel ∩ { 𝑥 ∣ ( 𝑋 ⊆ 𝑥 ∧ 𝜓 ) } )