dicfnN

Description: Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dicfn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	dicfn.a	$⊢ A = Atoms (K)$
	dicfn.h	$⊢ H = LHyp (K)$
	dicfn.i	$⊢ I = DIsoC (K) (W)$
Assertion	dicfnN	$⊢ (K \in V \land W \in H) \to I Fn \{p \in A \| \neg p \underset{˙}{\leq} W\}$

Proof

Step	Hyp	Ref	Expression
1		dicfn.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		dicfn.a	$⊢ A = Atoms (K)$
3		dicfn.h	$⊢ H = LHyp (K)$
4		dicfn.i	$⊢ I = DIsoC (K) (W)$
5		breq1	$⊢ p = q \to (p \underset{˙}{\leq} W \leftrightarrow q \underset{˙}{\leq} W)$
6	5	notbid	$⊢ p = q \to (\neg p \underset{˙}{\leq} W \leftrightarrow \neg q \underset{˙}{\leq} W)$
7	6	elrab	$⊢ q \in \{p \in A \| \neg p \underset{˙}{\leq} W\} \leftrightarrow (q \in A \land \neg q \underset{˙}{\leq} W)$
8		eqid	$⊢ oc (K) (W) = oc (K) (W)$
9		eqid	$⊢ LTrn (K) (W) = LTrn (K) (W)$
10		eqid	$⊢ TEndo (K) (W) = TEndo (K) (W)$
11	1 2 3 8 9 10 4	dicval	$⊢ ((K \in V \land W \in H) \land (q \in A \land \neg q \underset{˙}{\leq} W)) \to I (q) = \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\}$
12		fvex	$⊢ I (q) \in V$
13	11 12	eqeltrrdi	$⊢ ((K \in V \land W \in H) \land (q \in A \land \neg q \underset{˙}{\leq} W)) \to \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\} \in V$
14	7 13	sylan2b	$⊢ ((K \in V \land W \in H) \land q \in \{p \in A \| \neg p \underset{˙}{\leq} W\}) \to \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\} \in V$
15	14	ralrimiva	$⊢ (K \in V \land W \in H) \to \forall q \in \{p \in A \| \neg p \underset{˙}{\leq} W\} \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\} \in V$
16		eqid	$⊢ (q \in \{p \in A \| \neg p \underset{˙}{\leq} W\} ⟼ \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\}) = (q \in \{p \in A \| \neg p \underset{˙}{\leq} W\} ⟼ \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\})$
17	16	fnmpt	$⊢ \forall q \in \{p \in A \| \neg p \underset{˙}{\leq} W\} \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\} \in V \to (q \in \{p \in A \| \neg p \underset{˙}{\leq} W\} ⟼ \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\}) Fn \{p \in A \| \neg p \underset{˙}{\leq} W\}$
18	15 17	syl	$⊢ (K \in V \land W \in H) \to (q \in \{p \in A \| \neg p \underset{˙}{\leq} W\} ⟼ \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\}) Fn \{p \in A \| \neg p \underset{˙}{\leq} W\}$
19	1 2 3 8 9 10 4	dicfval	$⊢ (K \in V \land W \in H) \to I = (q \in \{p \in A \| \neg p \underset{˙}{\leq} W\} ⟼ \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\})$
20	19	fneq1d	$⊢ (K \in V \land W \in H) \to (I Fn \{p \in A \| \neg p \underset{˙}{\leq} W\} \leftrightarrow (q \in \{p \in A \| \neg p \underset{˙}{\leq} W\} ⟼ \{⟨f, s⟩ \| (f = s ((ι u \in LTrn (K) (W) \| u (oc (K) (W)) = q)) \land s \in TEndo (K) (W))\}) Fn \{p \in A \| \neg p \underset{˙}{\leq} W\})$
21	18 20	mpbird	$⊢ (K \in V \land W \in H) \to I Fn \{p \in A \| \neg p \underset{˙}{\leq} W\}$

Metamath Proof Explorer

Theorem dicfnN

Proof