dibvalrel

Description: The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014)

	Ref	Expression
Hypotheses	dibcl.h	$⊢ H = LHyp (K)$
	dibcl.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibvalrel	$⊢ (K \in V \land W \in H) \to Rel I (X)$

Proof

Step	Hyp	Ref	Expression
1		dibcl.h	$⊢ H = LHyp (K)$
2		dibcl.i	$⊢ I = DIsoB (K) (W)$
3		relxp	$⊢ Rel (DIsoA (K) (W) (X) \times \{(h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\})$
4		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
5	1 4 2	dibdiadm	$⊢ (K \in V \land W \in H) \to dom I = dom DIsoA (K) (W)$
6	5	eleq2d	$⊢ (K \in V \land W \in H) \to (X \in dom I \leftrightarrow X \in dom DIsoA (K) (W))$
7	6	biimpa	$⊢ ((K \in V \land W \in H) \land X \in dom I) \to X \in dom DIsoA (K) (W)$
8		eqid	$⊢ {Base}_{K} = {Base}_{K}$
9		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
10		eqid	$⊢ (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}}) = (h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})$
11	8 1 9 10 4 2	dibval	$⊢ ((K \in V \land W \in H) \land X \in dom DIsoA (K) (W)) \to I (X) = DIsoA (K) (W) (X) \times \{(h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\}$
12	7 11	syldan	$⊢ ((K \in V \land W \in H) \land X \in dom I) \to I (X) = DIsoA (K) (W) (X) \times \{(h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\}$
13	12	releqd	$⊢ ((K \in V \land W \in H) \land X \in dom I) \to (Rel I (X) \leftrightarrow Rel (DIsoA (K) (W) (X) \times \{(h \in LTrn (K) (W) ⟼ {I ↾}_{{Base}_{K}})\}))$
14	3 13	mpbiri	$⊢ ((K \in V \land W \in H) \land X \in dom I) \to Rel I (X)$
15		rel0	$⊢ Rel \emptyset$
16		ndmfv	$⊢ \neg X \in dom I \to I (X) = \emptyset$
17	16	releqd	$⊢ \neg X \in dom I \to (Rel I (X) \leftrightarrow Rel \emptyset)$
18	15 17	mpbiri	$⊢ \neg X \in dom I \to Rel I (X)$
19	18	adantl	$⊢ ((K \in V \land W \in H) \land \neg X \in dom I) \to Rel I (X)$
20	14 19	pm2.61dan	$⊢ (K \in V \land W \in H) \to Rel I (X)$

Metamath Proof Explorer

Theorem dibvalrel

Proof