dibelval3

Description: Member of the partial isomorphism B. (Contributed by NM, 26-Feb-2014)

	Ref	Expression
Hypotheses	dibval3.b	$⊢ B = {Base}_{K}$
	dibval3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dibval3.h	$⊢ H = LHyp (K)$
	dibval3.t	$⊢ T = LTrn (K) (W)$
	dibval3.r	$⊢ R = trL (K) (W)$
	dibval3.o	$⊢ \underset{˙}{0} = (g \in T ⟼ {I ↾}_{B})$
	dibval3.i	$⊢ I = DIsoB (K) (W)$
Assertion	dibelval3	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (Y \in I (X) \leftrightarrow \exists f \in T (Y = ⟨f, \underset{˙}{0}⟩ \land R (f) \underset{˙}{\leq} X))$

Proof

Step	Hyp	Ref	Expression
1		dibval3.b	$⊢ B = {Base}_{K}$
2		dibval3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		dibval3.h	$⊢ H = LHyp (K)$
4		dibval3.t	$⊢ T = LTrn (K) (W)$
5		dibval3.r	$⊢ R = trL (K) (W)$
6		dibval3.o	$⊢ \underset{˙}{0} = (g \in T ⟼ {I ↾}_{B})$
7		dibval3.i	$⊢ I = DIsoB (K) (W)$
8		eqid	$⊢ DIsoA (K) (W) = DIsoA (K) (W)$
9	1 2 3 4 6 8 7	dibval2	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to I (X) = DIsoA (K) (W) (X) \times \{\underset{˙}{0}\}$
10	9	eleq2d	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (Y \in I (X) \leftrightarrow Y \in (DIsoA (K) (W) (X) \times \{\underset{˙}{0}\}))$
11	1 2 3 4 5 8	diaelval	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (f \in DIsoA (K) (W) (X) \leftrightarrow (f \in T \land R (f) \underset{˙}{\leq} X))$
12	11	anbi1d	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to ((f \in DIsoA (K) (W) (X) \land Y = ⟨f, \underset{˙}{0}⟩) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} X) \land Y = ⟨f, \underset{˙}{0}⟩))$
13		an13	$⊢ (Y = ⟨f, s⟩ \land (f \in DIsoA (K) (W) (X) \land s \in \{\underset{˙}{0}\})) \leftrightarrow (s \in \{\underset{˙}{0}\} \land (f \in DIsoA (K) (W) (X) \land Y = ⟨f, s⟩))$
14		velsn	$⊢ s \in \{\underset{˙}{0}\} \leftrightarrow s = \underset{˙}{0}$
15	14	anbi1i	$⊢ (s \in \{\underset{˙}{0}\} \land (f \in DIsoA (K) (W) (X) \land Y = ⟨f, s⟩)) \leftrightarrow (s = \underset{˙}{0} \land (f \in DIsoA (K) (W) (X) \land Y = ⟨f, s⟩))$
16	13 15	bitri	$⊢ (Y = ⟨f, s⟩ \land (f \in DIsoA (K) (W) (X) \land s \in \{\underset{˙}{0}\})) \leftrightarrow (s = \underset{˙}{0} \land (f \in DIsoA (K) (W) (X) \land Y = ⟨f, s⟩))$
17	16	exbii	$⊢ \exists s (Y = ⟨f, s⟩ \land (f \in DIsoA (K) (W) (X) \land s \in \{\underset{˙}{0}\})) \leftrightarrow \exists s (s = \underset{˙}{0} \land (f \in DIsoA (K) (W) (X) \land Y = ⟨f, s⟩))$
18	4	fvexi	$⊢ T \in V$
19	18	mptex	$⊢ (g \in T ⟼ {I ↾}_{B}) \in V$
20	6 19	eqeltri	$⊢ \underset{˙}{0} \in V$
21		opeq2	$⊢ s = \underset{˙}{0} \to ⟨f, s⟩ = ⟨f, \underset{˙}{0}⟩$
22	21	eqeq2d	$⊢ s = \underset{˙}{0} \to (Y = ⟨f, s⟩ \leftrightarrow Y = ⟨f, \underset{˙}{0}⟩)$
23	22	anbi2d	$⊢ s = \underset{˙}{0} \to ((f \in DIsoA (K) (W) (X) \land Y = ⟨f, s⟩) \leftrightarrow (f \in DIsoA (K) (W) (X) \land Y = ⟨f, \underset{˙}{0}⟩))$
24	20 23	ceqsexv	$⊢ \exists s (s = \underset{˙}{0} \land (f \in DIsoA (K) (W) (X) \land Y = ⟨f, s⟩)) \leftrightarrow (f \in DIsoA (K) (W) (X) \land Y = ⟨f, \underset{˙}{0}⟩)$
25	17 24	bitri	$⊢ \exists s (Y = ⟨f, s⟩ \land (f \in DIsoA (K) (W) (X) \land s \in \{\underset{˙}{0}\})) \leftrightarrow (f \in DIsoA (K) (W) (X) \land Y = ⟨f, \underset{˙}{0}⟩)$
26		anass	$⊢ ((f \in T \land Y = ⟨f, \underset{˙}{0}⟩) \land R (f) \underset{˙}{\leq} X) \leftrightarrow (f \in T \land (Y = ⟨f, \underset{˙}{0}⟩ \land R (f) \underset{˙}{\leq} X))$
27		an32	$⊢ ((f \in T \land Y = ⟨f, \underset{˙}{0}⟩) \land R (f) \underset{˙}{\leq} X) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} X) \land Y = ⟨f, \underset{˙}{0}⟩)$
28	26 27	bitr3i	$⊢ (f \in T \land (Y = ⟨f, \underset{˙}{0}⟩ \land R (f) \underset{˙}{\leq} X)) \leftrightarrow ((f \in T \land R (f) \underset{˙}{\leq} X) \land Y = ⟨f, \underset{˙}{0}⟩)$
29	12 25 28	3bitr4g	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (\exists s (Y = ⟨f, s⟩ \land (f \in DIsoA (K) (W) (X) \land s \in \{\underset{˙}{0}\})) \leftrightarrow (f \in T \land (Y = ⟨f, \underset{˙}{0}⟩ \land R (f) \underset{˙}{\leq} X)))$
30	29	exbidv	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (\exists f \exists s (Y = ⟨f, s⟩ \land (f \in DIsoA (K) (W) (X) \land s \in \{\underset{˙}{0}\})) \leftrightarrow \exists f (f \in T \land (Y = ⟨f, \underset{˙}{0}⟩ \land R (f) \underset{˙}{\leq} X)))$
31		elxp	$⊢ Y \in (DIsoA (K) (W) (X) \times \{\underset{˙}{0}\}) \leftrightarrow \exists f \exists s (Y = ⟨f, s⟩ \land (f \in DIsoA (K) (W) (X) \land s \in \{\underset{˙}{0}\}))$
32		df-rex	$⊢ \exists f \in T (Y = ⟨f, \underset{˙}{0}⟩ \land R (f) \underset{˙}{\leq} X) \leftrightarrow \exists f (f \in T \land (Y = ⟨f, \underset{˙}{0}⟩ \land R (f) \underset{˙}{\leq} X))$
33	30 31 32	3bitr4g	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (Y \in (DIsoA (K) (W) (X) \times \{\underset{˙}{0}\}) \leftrightarrow \exists f \in T (Y = ⟨f, \underset{˙}{0}⟩ \land R (f) \underset{˙}{\leq} X))$
34	10 33	bitrd	$⊢ ((K \in V \land W \in H) \land (X \in B \land X \underset{˙}{\leq} W)) \to (Y \in I (X) \leftrightarrow \exists f \in T (Y = ⟨f, \underset{˙}{0}⟩ \land R (f) \underset{˙}{\leq} X))$

Metamath Proof Explorer

Theorem dibelval3

Proof