dicelval3

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

	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	dicelval3	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \leftrightarrow \exists s \in E Y = ⟨s (G), s⟩)$

Proof

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 8	dicval2	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to I (Q) = \{⟨f, s⟩ \| (f = s (G) \land s \in E)\}$
10	9	eleq2d	$⊢ ((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 \{⟨f, s⟩ \| (f = s (G) \land s \in E)\})$
11		excom	$⊢ \exists f \exists s (Y = ⟨f, s⟩ \land (f = s (G) \land s \in E)) \leftrightarrow \exists s \exists f (Y = ⟨f, s⟩ \land (f = s (G) \land s \in E))$
12		an12	$⊢ (Y = ⟨f, s⟩ \land (f = s (G) \land s \in E)) \leftrightarrow (f = s (G) \land (Y = ⟨f, s⟩ \land s \in E))$
13	12	exbii	$⊢ \exists f (Y = ⟨f, s⟩ \land (f = s (G) \land s \in E)) \leftrightarrow \exists f (f = s (G) \land (Y = ⟨f, s⟩ \land s \in E))$
14		fvex	$⊢ s (G) \in V$
15		opeq1	$⊢ f = s (G) \to ⟨f, s⟩ = ⟨s (G), s⟩$
16	15	eqeq2d	$⊢ f = s (G) \to (Y = ⟨f, s⟩ \leftrightarrow Y = ⟨s (G), s⟩)$
17	16	anbi1d	$⊢ f = s (G) \to ((Y = ⟨f, s⟩ \land s \in E) \leftrightarrow (Y = ⟨s (G), s⟩ \land s \in E))$
18	14 17	ceqsexv	$⊢ \exists f (f = s (G) \land (Y = ⟨f, s⟩ \land s \in E)) \leftrightarrow (Y = ⟨s (G), s⟩ \land s \in E)$
19		ancom	$⊢ (Y = ⟨s (G), s⟩ \land s \in E) \leftrightarrow (s \in E \land Y = ⟨s (G), s⟩)$
20	13 18 19	3bitri	$⊢ \exists f (Y = ⟨f, s⟩ \land (f = s (G) \land s \in E)) \leftrightarrow (s \in E \land Y = ⟨s (G), s⟩)$
21	20	exbii	$⊢ \exists s \exists f (Y = ⟨f, s⟩ \land (f = s (G) \land s \in E)) \leftrightarrow \exists s (s \in E \land Y = ⟨s (G), s⟩)$
22	11 21	bitri	$⊢ \exists f \exists s (Y = ⟨f, s⟩ \land (f = s (G) \land s \in E)) \leftrightarrow \exists s (s \in E \land Y = ⟨s (G), s⟩)$
23		elopab	$⊢ Y \in \{⟨f, s⟩ \| (f = s (G) \land s \in E)\} \leftrightarrow \exists f \exists s (Y = ⟨f, s⟩ \land (f = s (G) \land s \in E))$
24		df-rex	$⊢ \exists s \in E Y = ⟨s (G), s⟩ \leftrightarrow \exists s (s \in E \land Y = ⟨s (G), s⟩)$
25	22 23 24	3bitr4i	$⊢ Y \in \{⟨f, s⟩ \| (f = s (G) \land s \in E)\} \leftrightarrow \exists s \in E Y = ⟨s (G), s⟩$
26	10 25	syl6bb	$⊢ ((K \in V \land W \in H) \land (Q \in A \land \neg Q \underset{˙}{\leq} W)) \to (Y \in I (Q) \leftrightarrow \exists s \in E Y = ⟨s (G), s⟩)$

Metamath Proof Explorer

Theorem dicelval3

Proof