# Metamath Proof Explorer

## Theorem mptrcllem

Description: Show two versions of a closure with reflexive properties are equal. (Contributed by RP, 19-Oct-2020)

Ref Expression
Hypotheses mptrcllem.ex1 ${⊢}{x}\in {V}\to \bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}\in \mathrm{V}$
mptrcllem.ex2 ${⊢}{x}\in {V}\to \bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\in \mathrm{V}$
mptrcllem.hyp1 ${⊢}{x}\in {V}\to {\chi }$
mptrcllem.hyp2 ${⊢}{x}\in {V}\to {\theta }$
mptrcllem.hyp3 ${⊢}{x}\in {V}\to {\tau }$
mptrcllem.sub1 ${⊢}{y}=\bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\to \left({\phi }↔{\chi }\right)$
mptrcllem.sub2 ${⊢}{y}=\bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\to \left({\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}↔{\theta }\right)$
mptrcllem.sub3 ${⊢}{z}=\bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}\to \left({\psi }↔{\tau }\right)$
Assertion mptrcllem ${⊢}\left({x}\in {V}⟼\bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}\right)=\left({x}\in {V}⟼\bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\right)$

### Proof

Step Hyp Ref Expression
1 mptrcllem.ex1 ${⊢}{x}\in {V}\to \bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}\in \mathrm{V}$
2 mptrcllem.ex2 ${⊢}{x}\in {V}\to \bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\in \mathrm{V}$
3 mptrcllem.hyp1 ${⊢}{x}\in {V}\to {\chi }$
4 mptrcllem.hyp2 ${⊢}{x}\in {V}\to {\theta }$
5 mptrcllem.hyp3 ${⊢}{x}\in {V}\to {\tau }$
6 mptrcllem.sub1 ${⊢}{y}=\bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\to \left({\phi }↔{\chi }\right)$
7 mptrcllem.sub2 ${⊢}{y}=\bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\to \left({\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}↔{\theta }\right)$
8 mptrcllem.sub3 ${⊢}{z}=\bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}\to \left({\psi }↔{\tau }\right)$
9 6 7 anbi12d ${⊢}{y}=\bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\to \left(\left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)↔\left({\chi }\wedge {\theta }\right)\right)$
10 id ${⊢}{x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\to {x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}$
11 10 unssad ${⊢}{x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\to {x}\subseteq {z}$
12 11 adantr ${⊢}\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\to {x}\subseteq {z}$
13 12 a1i ${⊢}{x}\in {V}\to \left(\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\to {x}\subseteq {z}\right)$
14 13 alrimiv ${⊢}{x}\in {V}\to \forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\to {x}\subseteq {z}\right)$
15 ssintab ${⊢}{x}\subseteq \bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}↔\forall {z}\phantom{\rule{.4em}{0ex}}\left(\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\to {x}\subseteq {z}\right)$
16 14 15 sylibr ${⊢}{x}\in {V}\to {x}\subseteq \bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}$
17 3 4 jca ${⊢}{x}\in {V}\to \left({\chi }\wedge {\theta }\right)$
18 2 9 16 17 clublem ${⊢}{x}\in {V}\to \bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}\subseteq \bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}$
19 simpl ${⊢}\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\to {x}\subseteq {y}$
20 dmss ${⊢}{x}\subseteq {y}\to \mathrm{dom}{x}\subseteq \mathrm{dom}{y}$
21 rnss ${⊢}{x}\subseteq {y}\to \mathrm{ran}{x}\subseteq \mathrm{ran}{y}$
22 20 21 jca ${⊢}{x}\subseteq {y}\to \left(\mathrm{dom}{x}\subseteq \mathrm{dom}{y}\wedge \mathrm{ran}{x}\subseteq \mathrm{ran}{y}\right)$
23 unss12 ${⊢}\left(\mathrm{dom}{x}\subseteq \mathrm{dom}{y}\wedge \mathrm{ran}{x}\subseteq \mathrm{ran}{y}\right)\to \mathrm{dom}{x}\cup \mathrm{ran}{x}\subseteq \mathrm{dom}{y}\cup \mathrm{ran}{y}$
24 ssres2 ${⊢}\mathrm{dom}{x}\cup \mathrm{ran}{x}\subseteq \mathrm{dom}{y}\cup \mathrm{ran}{y}\to {\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\subseteq {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}$
25 22 23 24 3syl ${⊢}{x}\subseteq {y}\to {\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\subseteq {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}$
26 25 adantr ${⊢}\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\to {\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\subseteq {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}$
27 simprr ${⊢}\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\to {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}$
28 26 27 sstrd ${⊢}\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\to {\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\subseteq {y}$
29 19 28 jca ${⊢}\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\to \left({x}\subseteq {y}\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\subseteq {y}\right)$
30 29 a1i ${⊢}{x}\in {V}\to \left(\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\to \left({x}\subseteq {y}\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\subseteq {y}\right)\right)$
31 unss ${⊢}\left({x}\subseteq {y}\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\subseteq {y}\right)↔{x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {y}$
32 30 31 syl6ib ${⊢}{x}\in {V}\to \left(\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\to {x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {y}\right)$
33 32 alrimiv ${⊢}{x}\in {V}\to \forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\to {x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {y}\right)$
34 ssintab ${⊢}{x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq \bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\to {x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {y}\right)$
35 33 34 sylibr ${⊢}{x}\in {V}\to {x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq \bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}$
36 1 8 35 5 clublem ${⊢}{x}\in {V}\to \bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\subseteq \bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}$
37 18 36 eqssd ${⊢}{x}\in {V}\to \bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}=\bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}$
38 37 mpteq2ia ${⊢}\left({x}\in {V}⟼\bigcap \left\{{y}|\left({x}\subseteq {y}\wedge \left({\phi }\wedge {\mathrm{I}↾}_{\left(\mathrm{dom}{y}\cup \mathrm{ran}{y}\right)}\subseteq {y}\right)\right)\right\}\right)=\left({x}\in {V}⟼\bigcap \left\{{z}|\left({x}\cup \left({\mathrm{I}↾}_{\left(\mathrm{dom}{x}\cup \mathrm{ran}{x}\right)}\right)\subseteq {z}\wedge {\psi }\right)\right\}\right)$