dicelval2N

Description: Membership in value of the partial isomorphism C for a lattice K . (Contributed by NM, 25-Feb-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dicval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dicval.a	$⊢ A = Atoms (K)$
	dicval.h	$⊢ H = LHyp (K)$
	dicval.p	$⊢ P = oc (K) (W)$
	dicval.t	$⊢ T = LTrn (K) (W)$
	dicval.e	$⊢ E = TEndo (K) (W)$
	dicval.i	$⊢ I = DIsoC (K) (W)$
	dicval2.g	$⊢ G = (ι g \in T \| g (P) = Q)$
Assertion	dicelval2N	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \leftrightarrow (Y \in (V \times V) \land (1^{st} (Y) = 2^{nd} (Y) (G) \land 2^{nd} (Y) \in E)))$

Step	Hyp	Ref	Expression
1		dicval.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicval.a	$⊢ A = Atoms (K)$
3		dicval.h	$⊢ H = LHyp (K)$
4		dicval.p	$⊢ P = oc (K) (W)$
5		dicval.t	$⊢ T = LTrn (K) (W)$
6		dicval.e	$⊢ E = TEndo (K) (W)$
7		dicval.i	$⊢ I = DIsoC (K) (W)$
8		dicval2.g	$⊢ G = (ι g \in T \| g (P) = Q)$
9	1 2 3 4 5 6 7	dicelvalN	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \leftrightarrow (Y \in (V \times V) \land (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \in E)))$
10	8	fveq2i	$⊢ 2^{nd} (Y) (G) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q))$
11	10	eqeq2i	$⊢ 1^{st} (Y) = 2^{nd} (Y) (G) \leftrightarrow 1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q))$
12	11	anbi1i	$⊢ (1^{st} (Y) = 2^{nd} (Y) (G) \land 2^{nd} (Y) \in E) \leftrightarrow (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \in E)$
13	12	anbi2i	$⊢ (Y \in (V \times V) \land (1^{st} (Y) = 2^{nd} (Y) (G) \land 2^{nd} (Y) \in E)) \leftrightarrow (Y \in (V \times V) \land (1^{st} (Y) = 2^{nd} (Y) ((ι g \in T \| g (P) = Q)) \land 2^{nd} (Y) \in E))$
14	9 13	bitr4di	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \leftrightarrow (Y \in (V \times V) \land (1^{st} (Y) = 2^{nd} (Y) (G) \land 2^{nd} (Y) \in E)))$

Metamath Proof Explorer