dvcnp2

Description: A function is continuous at each point for which it is differentiable. (Contributed by Mario Carneiro, 9-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	dvcnp.j	$⊢ J = K ↾_{𝑡} A$
	dvcnp.k	$⊢ K = TopOpen (ℂ_{fld})$
Assertion	dvcnp2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to F \in (J CnP K) (B)$

Proof

Step	Hyp	Ref	Expression
1		dvcnp.j	$⊢ J = K ↾_{𝑡} A$
2		dvcnp.k	$⊢ K = TopOpen (ℂ_{fld})$
3		simpl2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F : A ⟶ ℂ$
4	3	ffvelrnda	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in A) \to F (z) \in ℂ$
5	2	cnfldtop	$⊢ K \in Top$
6		simpl1	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to S \subseteq ℂ$
7		cnex	$⊢ ℂ \in V$
8		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
9	6 7 8	sylancl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to S \in V$
10		resttop	$⊢ (K \in Top \land S \in V) \to K ↾_{𝑡} S \in Top$
11	5 9 10	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to K ↾_{𝑡} S \in Top$
12		simpl3	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to A \subseteq S$
13	2	cnfldtopon	$⊢ K \in TopOn (ℂ)$
14		resttopon	$⊢ (K \in TopOn (ℂ) \land S \subseteq ℂ) \to K ↾_{𝑡} S \in TopOn (S)$
15	13 6 14	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to K ↾_{𝑡} S \in TopOn (S)$
16		toponuni	$⊢ K ↾_{𝑡} S \in TopOn (S) \to S = ⋃ (K ↾_{𝑡} S)$
17	15 16	syl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to S = ⋃ (K ↾_{𝑡} S)$
18	12 17	sseqtrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to A \subseteq ⋃ (K ↾_{𝑡} S)$
19		eqid	$⊢ ⋃ (K ↾_{𝑡} S) = ⋃ (K ↾_{𝑡} S)$
20	19	ntrss2	$⊢ (K ↾_{𝑡} S \in Top \land A \subseteq ⋃ (K ↾_{𝑡} S)) \to int (K ↾_{𝑡} S) (A) \subseteq A$
21	11 18 20	syl2anc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to int (K ↾_{𝑡} S) (A) \subseteq A$
22		eqid	$⊢ K ↾_{𝑡} S = K ↾_{𝑡} S$
23		eqid	$⊢ (z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) = (z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B})$
24		simp1	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to S \subseteq ℂ$
25		simp2	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to F : A ⟶ ℂ$
26		simp3	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to A \subseteq S$
27	22 2 23 24 25 26	eldv	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (B F_{S}^{'} y \leftrightarrow (B \in int (K ↾_{𝑡} S) (A) \land y \in ((z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) {lim}_{ℂ} B)))$
28	27	simprbda	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B \in int (K ↾_{𝑡} S) (A)$
29	21 28	sseldd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B \in A$
30	3 29	ffvelrnd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F (B) \in ℂ$
31	30	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in A) \to F (B) \in ℂ$
32	4 31	subcld	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in A) \to F (z) - F (B) \in ℂ$
33		ssid	$⊢ ℂ \subseteq ℂ$
34	33	a1i	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to ℂ \subseteq ℂ$
35		txtopon	$⊢ (K \in TopOn (ℂ) \land K \in TopOn (ℂ)) \to K \times_{t} K \in TopOn (ℂ \times ℂ)$
36	13 13 35	mp2an	$⊢ K \times_{t} K \in TopOn (ℂ \times ℂ)$
37	36	toponrestid	$⊢ K \times_{t} K = (K \times_{t} K) ↾_{𝑡} (ℂ \times ℂ)$
38	12 6	sstrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to A \subseteq ℂ$
39	3 38 29	dvlem	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to \frac{F (z) - F (B)}{z - B} \in ℂ$
40	38	ssdifssd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to A ∖ \{B\} \subseteq ℂ$
41	40	sselda	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z \in ℂ$
42	38 29	sseldd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B \in ℂ$
43	42	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to B \in ℂ$
44	41 43	subcld	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z - B \in ℂ$
45	27	simplbda	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y \in ((z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) {lim}_{ℂ} B)$
46		limcresi	$⊢ (z \in A ⟼ z - B) {lim}_{ℂ} B \subseteq ({(z \in A ⟼ z - B) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B$
47		difss	$⊢ A ∖ \{B\} \subseteq A$
48		resmpt	$⊢ A ∖ \{B\} \subseteq A \to {(z \in A ⟼ z - B) ↾}_{(A ∖ \{B\})} = (z \in (A ∖ \{B\}) ⟼ z - B)$
49	47 48	ax-mp	$⊢ {(z \in A ⟼ z - B) ↾}_{(A ∖ \{B\})} = (z \in (A ∖ \{B\}) ⟼ z - B)$
50	49	oveq1i	$⊢ ({(z \in A ⟼ z - B) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B = (z \in (A ∖ \{B\}) ⟼ z - B) {lim}_{ℂ} B$
51	46 50	sseqtri	$⊢ (z \in A ⟼ z - B) {lim}_{ℂ} B \subseteq (z \in (A ∖ \{B\}) ⟼ z - B) {lim}_{ℂ} B$
52	42	subidd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B - B = 0$
53	2	subcn	$⊢ - \in ((K \times_{t} K) Cn K)$
54	53	a1i	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to - \in ((K \times_{t} K) Cn K)$
55		cncfmptid	$⊢ (A \subseteq ℂ \land ℂ \subseteq ℂ) \to (z \in A ⟼ z) : A \underset{cn}{⟶} ℂ$
56	38 33 55	sylancl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ z) : A \underset{cn}{⟶} ℂ$
57		cncfmptc	$⊢ (B \in ℂ \land A \subseteq ℂ \land ℂ \subseteq ℂ) \to (z \in A ⟼ B) : A \underset{cn}{⟶} ℂ$
58	42 38 34 57	syl3anc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ B) : A \underset{cn}{⟶} ℂ$
59	2 54 56 58	cncfmpt2f	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ z - B) : A \underset{cn}{⟶} ℂ$
60		oveq1	$⊢ z = B \to z - B = B - B$
61	59 29 60	cnmptlimc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to B - B \in ((z \in A ⟼ z - B) {lim}_{ℂ} B)$
62	52 61	eqeltrrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 \in ((z \in A ⟼ z - B) {lim}_{ℂ} B)$
63	51 62	sselid	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 \in ((z \in (A ∖ \{B\}) ⟼ z - B) {lim}_{ℂ} B)$
64	2	mulcn	$⊢ \times \in ((K \times_{t} K) Cn K)$
65	24 25 26	dvcl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y \in ℂ$
66		0cn	$⊢ 0 \in ℂ$
67		opelxpi	$⊢ (y \in ℂ \land 0 \in ℂ) \to ⟨y, 0⟩ \in (ℂ \times ℂ)$
68	65 66 67	sylancl	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to ⟨y, 0⟩ \in (ℂ \times ℂ)$
69	36	toponunii	$⊢ ℂ \times ℂ = ⋃ (K \times_{t} K)$
70	69	cncnpi	$⊢ (\times \in ((K \times_{t} K) Cn K) \land ⟨y, 0⟩ \in (ℂ \times ℂ)) \to \times \in ((K \times_{t} K) CnP K) (⟨y, 0⟩)$
71	64 68 70	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to \times \in ((K \times_{t} K) CnP K) (⟨y, 0⟩)$
72	39 44 34 34 2 37 45 63 71	limccnp2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y \cdot 0 \in ((z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (z - B)) {lim}_{ℂ} B)$
73	65	mul01d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to y \cdot 0 = 0$
74	3	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to F : A ⟶ ℂ$
75		simpr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z \in (A ∖ \{B\})$
76	47 75	sselid	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z \in A$
77	74 76	ffvelrnd	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to F (z) \in ℂ$
78	30	adantr	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to F (B) \in ℂ$
79	77 78	subcld	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to F (z) - F (B) \in ℂ$
80		eldifsni	$⊢ z \in (A ∖ \{B\}) \to z \neq B$
81	80	adantl	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z \neq B$
82	41 43 81	subne0d	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to z - B \neq 0$
83	79 44 82	divcan1d	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in (A ∖ \{B\})) \to (\frac{F (z) - F (B)}{z - B}) (z - B) = F (z) - F (B)$
84	83	mpteq2dva	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (z - B)) = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B))$
85	84	oveq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in (A ∖ \{B\}) ⟼ (\frac{F (z) - F (B)}{z - B}) (z - B)) {lim}_{ℂ} B = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B)) {lim}_{ℂ} B$
86	72 73 85	3eltr3d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 \in ((z \in (A ∖ \{B\}) ⟼ F (z) - F (B)) {lim}_{ℂ} B)$
87	32	fmpttd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B)) : A ⟶ ℂ$
88	87	limcdif	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B)) {lim}_{ℂ} B = ({(z \in A ⟼ F (z) - F (B)) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B$
89		resmpt	$⊢ A ∖ \{B\} \subseteq A \to {(z \in A ⟼ F (z) - F (B)) ↾}_{(A ∖ \{B\})} = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B))$
90	47 89	ax-mp	$⊢ {(z \in A ⟼ F (z) - F (B)) ↾}_{(A ∖ \{B\})} = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B))$
91	90	oveq1i	$⊢ ({(z \in A ⟼ F (z) - F (B)) ↾}_{(A ∖ \{B\})}) {lim}_{ℂ} B = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B)) {lim}_{ℂ} B$
92	88 91	eqtrdi	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B)) {lim}_{ℂ} B = (z \in (A ∖ \{B\}) ⟼ F (z) - F (B)) {lim}_{ℂ} B$
93	86 92	eleqtrrd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 \in ((z \in A ⟼ F (z) - F (B)) {lim}_{ℂ} B)$
94		cncfmptc	$⊢ (F (B) \in ℂ \land A \subseteq ℂ \land ℂ \subseteq ℂ) \to (z \in A ⟼ F (B)) : A \underset{cn}{⟶} ℂ$
95	30 38 34 94	syl3anc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (B)) : A \underset{cn}{⟶} ℂ$
96		eqidd	$⊢ z = B \to F (B) = F (B)$
97	95 29 96	cnmptlimc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F (B) \in ((z \in A ⟼ F (B)) {lim}_{ℂ} B)$
98	2	addcn	$⊢ + \in ((K \times_{t} K) Cn K)$
99		opelxpi	$⊢ (0 \in ℂ \land F (B) \in ℂ) \to ⟨0, F (B)⟩ \in (ℂ \times ℂ)$
100	66 30 99	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to ⟨0, F (B)⟩ \in (ℂ \times ℂ)$
101	69	cncnpi	$⊢ (+ \in ((K \times_{t} K) Cn K) \land ⟨0, F (B)⟩ \in (ℂ \times ℂ)) \to + \in ((K \times_{t} K) CnP K) (⟨0, F (B)⟩)$
102	98 100 101	sylancr	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to + \in ((K \times_{t} K) CnP K) (⟨0, F (B)⟩)$
103	32 31 34 34 2 37 93 97 102	limccnp2	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 + F (B) \in ((z \in A ⟼ F (z) - F (B) + F (B)) {lim}_{ℂ} B)$
104	30	addid2d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to 0 + F (B) = F (B)$
105	4 31	npcand	$⊢ (((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \land z \in A) \to F (z) - F (B) + F (B) = F (z)$
106	105	mpteq2dva	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B) + F (B)) = (z \in A ⟼ F (z))$
107	3	feqmptd	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F = (z \in A ⟼ F (z))$
108	106 107	eqtr4d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B) + F (B)) = F$
109	108	oveq1d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (z \in A ⟼ F (z) - F (B) + F (B)) {lim}_{ℂ} B = F {lim}_{ℂ} B$
110	103 104 109	3eltr3d	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F (B) \in (F {lim}_{ℂ} B)$
111	2 1	cnplimc	$⊢ (A \subseteq ℂ \land B \in A) \to (F \in (J CnP K) (B) \leftrightarrow (F : A ⟶ ℂ \land F (B) \in (F {lim}_{ℂ} B)))$
112	38 29 111	syl2anc	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to (F \in (J CnP K) (B) \leftrightarrow (F : A ⟶ ℂ \land F (B) \in (F {lim}_{ℂ} B)))$
113	3 110 112	mpbir2and	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B F_{S}^{'} y) \to F \in (J CnP K) (B)$
114	113	ex	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (B F_{S}^{'} y \to F \in (J CnP K) (B))$
115	114	exlimdv	$⊢ (S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \to (\exists y B F_{S}^{'} y \to F \in (J CnP K) (B))$
116		eldmg	$⊢ B \in dom F_{S}^{'} \to (B \in dom F_{S}^{'} \leftrightarrow \exists y B F_{S}^{'} y)$
117	116	ibi	$⊢ B \in dom F_{S}^{'} \to \exists y B F_{S}^{'} y$
118	115 117	impel	$⊢ ((S \subseteq ℂ \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to F \in (J CnP K) (B)$

Metamath Proof Explorer

Theorem dvcnp2

Proof