Metamath Proof Explorer

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 ⊢ φ → Y ∈ V
clrellem.rel ⊢ φ → Rel ⁡ X
clrellem.sub ⊢ x = Y -1 -1 → ψ ↔ χ
clrellem.sup ⊢ φ → X ⊆ Y
clrellem.maj ⊢ φ → χ
Assertion clrellem ⊢ φ → Rel ⁡ ⋂ x | X ⊆ x ∧ ψ

Proof

Step Hyp Ref Expression
1 clrellem.y ⊢ φ → Y ∈ V
2 clrellem.rel ⊢ φ → Rel ⁡ X
3 clrellem.sub ⊢ x = Y -1 -1 → ψ ↔ χ
4 clrellem.sup ⊢ φ → X ⊆ Y
5 clrellem.maj ⊢ φ → χ
6 cnvexg ⊢ Y ∈ V → Y -1 ∈ V
7 cnvexg ⊢ Y -1 ∈ V → Y -1 -1 ∈ V
8 1 6 7 3syl ⊢ φ → Y -1 -1 ∈ V
9 dfrel2 ⊢ Rel ⁡ X ↔ X -1 -1 = X
10 2 9 sylib ⊢ φ → X -1 -1 = X
11 cnvss ⊢ X ⊆ Y → X -1 ⊆ Y -1
12 cnvss ⊢ X -1 ⊆ Y -1 → X -1 -1 ⊆ Y -1 -1
13 4 11 12 3syl ⊢ φ → X -1 -1 ⊆ Y -1 -1
14 10 13 eqsstrrd ⊢ φ → X ⊆ Y -1 -1
15 relcnv ⊢ Rel ⁡ Y -1 -1
16 15 a1i ⊢ φ → Rel ⁡ Y -1 -1
17 14 5 16 jca31 ⊢ φ → X ⊆ Y -1 -1 ∧ χ ∧ Rel ⁡ Y -1 -1
18 3 cleq2lem ⊢ x = Y -1 -1 → X ⊆ x ∧ ψ ↔ X ⊆ Y -1 -1 ∧ χ
19 releq ⊢ x = Y -1 -1 → Rel ⁡ x ↔ Rel ⁡ Y -1 -1
20 18 19 anbi12d ⊢ x = Y -1 -1 → X ⊆ x ∧ ψ ∧ Rel ⁡ x ↔ X ⊆ Y -1 -1 ∧ χ ∧ Rel ⁡ Y -1 -1
21 8 17 20 spcedv ⊢ φ → ∃ x X ⊆ x ∧ ψ ∧ Rel ⁡ x
22 releq ⊢ y = x → Rel ⁡ y ↔ Rel ⁡ x
23 22 rexab2 ⊢ ∃ y ∈ x | X ⊆ x ∧ ψ Rel ⁡ y ↔ ∃ x X ⊆ x ∧ ψ ∧ Rel ⁡ x
24 23 biimpri ⊢ ∃ x X ⊆ x ∧ ψ ∧ Rel ⁡ x → ∃ y ∈ x | X ⊆ x ∧ ψ Rel ⁡ y
25 relint ⊢ ∃ y ∈ x | X ⊆ x ∧ ψ Rel ⁡ y → Rel ⁡ ⋂ x | X ⊆ x ∧ ψ
26 21 24 25 3syl ⊢ φ → Rel ⁡ ⋂ x | X ⊆ x ∧ ψ