diaeldm

Description: Member of domain of the partial isomorphism A. (Contributed by NM, 4-Dec-2013)

	Ref	Expression
Hypotheses	diafn.b	$⊢ B = {Base}_{K}$
	diafn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	diafn.h	$⊢ H = LHyp (K)$
	diafn.i	$⊢ I = DIsoA (K) (W)$
Assertion	diaeldm	$⊢ (K \in V \land W \in H) \to (X \in dom I \leftrightarrow (X \in B \land X \underset{˙}{\leq} W))$

Step	Hyp	Ref	Expression
1		diafn.b	$⊢ B = {Base}_{K}$
2		diafn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		diafn.h	$⊢ H = LHyp (K)$
4		diafn.i	$⊢ I = DIsoA (K) (W)$
5	1 2 3 4	diadm	$⊢ (K \in V \land W \in H) \to dom I = \{x \in B \| x \underset{˙}{\leq} W\}$
6	5	eleq2d	$⊢ (K \in V \land W \in H) \to (X \in dom I \leftrightarrow X \in \{x \in B \| x \underset{˙}{\leq} W\})$
7		breq1	$⊢ x = X \to (x \underset{˙}{\leq} W \leftrightarrow X \underset{˙}{\leq} W)$
8	7	elrab	$⊢ X \in \{x \in B \| x \underset{˙}{\leq} W\} \leftrightarrow (X \in B \land X \underset{˙}{\leq} W)$
9	6 8	bitrdi	$⊢ (K \in V \land W \in H) \to (X \in dom I \leftrightarrow (X \in B \land X \underset{˙}{\leq} W))$

Metamath Proof Explorer