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 ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \in V$
	mptrcllem.ex2	$⊢ x \in V \to ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\} \in V$
	mptrcllem.hyp1	$⊢ x \in V \to χ$
	mptrcllem.hyp2	$⊢ x \in V \to θ$
	mptrcllem.hyp3	$⊢ x \in V \to τ$
	mptrcllem.sub1	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\} \to (φ \leftrightarrow χ)$
	mptrcllem.sub2	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\} \to ({I ↾}_{(dom y \cup ran y)} \subseteq y \leftrightarrow θ)$
	mptrcllem.sub3	$⊢ z = ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \to (ψ \leftrightarrow τ)$
Assertion	mptrcllem	$⊢ (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}) = (x \in V ⟼ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\})$

Proof

Step	Hyp	Ref	Expression
1		mptrcllem.ex1	$⊢ x \in V \to ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \in V$
2		mptrcllem.ex2	$⊢ x \in V \to ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\} \in V$
3		mptrcllem.hyp1	$⊢ x \in V \to χ$
4		mptrcllem.hyp2	$⊢ x \in V \to θ$
5		mptrcllem.hyp3	$⊢ x \in V \to τ$
6		mptrcllem.sub1	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\} \to (φ \leftrightarrow χ)$
7		mptrcllem.sub2	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\} \to ({I ↾}_{(dom y \cup ran y)} \subseteq y \leftrightarrow θ)$
8		mptrcllem.sub3	$⊢ z = ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \to (ψ \leftrightarrow τ)$
9	6 7	anbi12d	$⊢ y = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\} \to ((φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y) \leftrightarrow (χ \land θ))$
10		id	$⊢ x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \to x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z$
11	10	unssad	$⊢ x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \to x \subseteq z$
12	11	adantr	$⊢ (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ) \to x \subseteq z$
13	12	a1i	$⊢ x \in V \to ((x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ) \to x \subseteq z)$
14	13	alrimiv	$⊢ x \in V \to \forall z ((x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ) \to x \subseteq z)$
15		ssintab	$⊢ x \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\} \leftrightarrow \forall z ((x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ) \to x \subseteq z)$
16	14 15	sylibr	$⊢ x \in V \to x \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\}$
17	3 4	jca	$⊢ x \in V \to (χ \land θ)$
18	2 9 16 17	clublem	$⊢ x \in V \to ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \subseteq ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\}$
19		simpl	$⊢ (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to x \subseteq y$
20		dmss	$⊢ x \subseteq y \to dom x \subseteq dom y$
21		rnss	$⊢ x \subseteq y \to ran x \subseteq ran y$
22	20 21	jca	$⊢ x \subseteq y \to (dom x \subseteq dom y \land ran x \subseteq ran y)$
23		unss12	$⊢ (dom x \subseteq dom y \land ran x \subseteq ran y) \to dom x \cup ran x \subseteq dom y \cup ran y$
24		ssres2	$⊢ dom x \cup ran x \subseteq dom y \cup ran y \to {I ↾}_{(dom x \cup ran x)} \subseteq {I ↾}_{(dom y \cup ran y)}$
25	22 23 24	3syl	$⊢ x \subseteq y \to {I ↾}_{(dom x \cup ran x)} \subseteq {I ↾}_{(dom y \cup ran y)}$
26	25	adantr	$⊢ (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to {I ↾}_{(dom x \cup ran x)} \subseteq {I ↾}_{(dom y \cup ran y)}$
27		simprr	$⊢ (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to {I ↾}_{(dom y \cup ran y)} \subseteq y$
28	26 27	sstrd	$⊢ (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to {I ↾}_{(dom x \cup ran x)} \subseteq y$
29	19 28	jca	$⊢ (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to (x \subseteq y \land {I ↾}_{(dom x \cup ran x)} \subseteq y)$
30	29	a1i	$⊢ x \in V \to ((x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to (x \subseteq y \land {I ↾}_{(dom x \cup ran x)} \subseteq y))$
31		unss	$⊢ (x \subseteq y \land {I ↾}_{(dom x \cup ran x)} \subseteq y) \leftrightarrow x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq y$
32	30 31	imbitrdi	$⊢ x \in V \to ((x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq y)$
33	32	alrimiv	$⊢ x \in V \to \forall y ((x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq y)$
34		ssintab	$⊢ x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} \leftrightarrow \forall y ((x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y)) \to x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq y)$
35	33 34	sylibr	$⊢ x \in V \to x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}$
36	1 8 35 5	clublem	$⊢ x \in V \to ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\} \subseteq ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}$
37	18 36	eqssd	$⊢ x \in V \to ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\} = ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\}$
38	37	mpteq2ia	$⊢ (x \in V ⟼ ⋂ \{y \| (x \subseteq y \land (φ \land {I ↾}_{(dom y \cup ran y)} \subseteq y))\}) = (x \in V ⟼ ⋂ \{z \| (x \cup ({I ↾}_{(dom x \cup ran x)}) \subseteq z \land ψ)\})$

Metamath Proof Explorer

Theorem mptrcllem

Proof