dicvalrelN

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

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

Proof

Step	Hyp	Ref	Expression
1		dicvalrel.h	$⊢ H = LHyp (K)$
2		dicvalrel.i	$⊢ I = DIsoC (K) (W)$
3		relopabv	$⊢ Rel \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = X)) \land s \in TEndo (K) (W))\}$
4		eqid	$⊢ \leq_{K} = \leq_{K}$
5		eqid	$⊢ Atoms (K) = Atoms (K)$
6	4 5 1 2	dicdmN	$⊢ (K \in V \land W \in H) \to dom I = \{p \in Atoms (K) \| \neg p \leq_{K} W\}$
7	6	eleq2d	$⊢ (K \in V \land W \in H) \to (X \in dom I \leftrightarrow X \in \{p \in Atoms (K) \| \neg p \leq_{K} W\})$
8		breq1	$⊢ p = X \to (p \leq_{K} W \leftrightarrow X \leq_{K} W)$
9	8	notbid	$⊢ p = X \to (\neg p \leq_{K} W \leftrightarrow \neg X \leq_{K} W)$
10	9	elrab	$⊢ X \in \{p \in Atoms (K) \| \neg p \leq_{K} W\} \leftrightarrow (X \in Atoms (K) \land \neg X \leq_{K} W)$
11	7 10	bitrdi	$⊢ (K \in V \land W \in H) \to (X \in dom I \leftrightarrow (X \in Atoms (K) \land \neg X \leq_{K} W))$
12	11	biimpa	$⊢ ((K \in V \land W \in H) \land X \in dom I) \to (X \in Atoms (K) \land \neg X \leq_{K} W)$
13		eqid	$⊢ oc (K) (W) = oc (K) (W)$
14		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
15		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
16	4 5 1 13 14 15 2	dicval	$⊢ ((K \in V \land W \in H) \land (X \in Atoms (K) \land \neg X \leq_{K} W)) \to I (X) = \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = X)) \land s \in TEndo (K) (W))\}$
17	12 16	syldan	$⊢ ((K \in V \land W \in H) \land X \in dom I) \to I (X) = \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = X)) \land s \in TEndo (K) (W))\}$
18	17	releqd	$⊢ ((K \in V \land W \in H) \land X \in dom I) \to (Rel I (X) \leftrightarrow Rel \{⟨f, s⟩ \| (f = s ((ι g \in LTrn (K) (W) \| g (oc (K) (W)) = X)) \land s \in TEndo (K) (W))\})$
19	3 18	mpbiri	$⊢ ((K \in V \land W \in H) \land X \in dom I) \to Rel I (X)$
20	19	ex	$⊢ (K \in V \land W \in H) \to (X \in dom I \to Rel I (X))$
21		rel0	$⊢ Rel \emptyset$
22		ndmfv	$⊢ \neg X \in dom I \to I (X) = \emptyset$
23	22	releqd	$⊢ \neg X \in dom I \to (Rel I (X) \leftrightarrow Rel \emptyset)$
24	21 23	mpbiri	$⊢ \neg X \in dom I \to Rel I (X)$
25	20 24	pm2.61d1	$⊢ (K \in V \land W \in H) \to Rel I (X)$

Metamath Proof Explorer

Theorem dicvalrelN

Proof