nelsubclem

	Ref	Expression
Hypotheses	nelsubc.b	$⊢ B = {Base}_{C}$
	nelsubc.s	$⊢ φ \to S \subseteq B$
	nelsubc.0	$⊢ φ \to S \neq \emptyset$
	nelsubc.j	$⊢ φ \to J = (S \times S) \times \{\emptyset\}$
	nelsubc.h	$⊢ H = {Hom}_{𝑓} (C)$
Assertion	nelsubclem	$⊢ φ \to (J Fn (S \times S) \land (J \subseteq_{cat} H \land (\neg \forall x \in S I \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) ψ)))$

Proof

Step	Hyp	Ref	Expression
1		nelsubc.b	$⊢ B = {Base}_{C}$
2		nelsubc.s	$⊢ φ \to S \subseteq B$
3		nelsubc.0	$⊢ φ \to S \neq \emptyset$
4		nelsubc.j	$⊢ φ \to J = (S \times S) \times \{\emptyset\}$
5		nelsubc.h	$⊢ H = {Hom}_{𝑓} (C)$
6		0ex	$⊢ \emptyset \in V$
7		fnconstg	$⊢ \emptyset \in V \to ((S \times S) \times \{\emptyset\}) Fn (S \times S)$
8	6 7	ax-mp	$⊢ ((S \times S) \times \{\emptyset\}) Fn (S \times S)$
9	4	fneq1d	$⊢ φ \to (J Fn (S \times S) \leftrightarrow ((S \times S) \times \{\emptyset\}) Fn (S \times S))$
10	8 9	mpbiri	$⊢ φ \to J Fn (S \times S)$
11	4	oveqd	$⊢ φ \to p J q = p ((S \times S) \times \{\emptyset\}) q$
12	6	ovconst2	$⊢ (p \in S \land q \in S) \to p ((S \times S) \times \{\emptyset\}) q = \emptyset$
13	11 12	sylan9eq	$⊢ (φ \land (p \in S \land q \in S)) \to p J q = \emptyset$
14		0ss	$⊢ \emptyset \subseteq p H q$
15	13 14	eqsstrdi	$⊢ (φ \land (p \in S \land q \in S)) \to p J q \subseteq p H q$
16	15	ralrimivva	$⊢ φ \to \forall p \in S \forall q \in S p J q \subseteq p H q$
17	5 1	homffn	$⊢ H Fn (B \times B)$
18	17	a1i	$⊢ φ \to H Fn (B \times B)$
19	1	fvexi	$⊢ B \in V$
20	19	a1i	$⊢ φ \to B \in V$
21	10 18 20	isssc	$⊢ φ \to (J \subseteq_{cat} H \leftrightarrow (S \subseteq B \land \forall p \in S \forall q \in S p J q \subseteq p H q))$
22	2 16 21	mpbir2and	$⊢ φ \to J \subseteq_{cat} H$
23	4	oveqd	$⊢ φ \to x J x = x ((S \times S) \times \{\emptyset\}) x$
24	6	ovconst2	$⊢ (x \in S \land x \in S) \to x ((S \times S) \times \{\emptyset\}) x = \emptyset$
25	24	anidms	$⊢ x \in S \to x ((S \times S) \times \{\emptyset\}) x = \emptyset$
26	23 25	sylan9eq	$⊢ (φ \land x \in S) \to x J x = \emptyset$
27		nel02	$⊢ x J x = \emptyset \to \neg I \in (x J x)$
28	26 27	syl	$⊢ (φ \land x \in S) \to \neg I \in (x J x)$
29	28	reximdva0	$⊢ (φ \land S \neq \emptyset) \to \exists x \in S \neg I \in (x J x)$
30	3 29	mpdan	$⊢ φ \to \exists x \in S \neg I \in (x J x)$
31		rexnal	$⊢ \exists x \in S \neg I \in (x J x) \leftrightarrow \neg \forall x \in S I \in (x J x)$
32	30 31	sylib	$⊢ φ \to \neg \forall x \in S I \in (x J x)$
33	4	oveqd	$⊢ φ \to x J y = x ((S \times S) \times \{\emptyset\}) y$
34	6	ovconst2	$⊢ (x \in S \land y \in S) \to x ((S \times S) \times \{\emptyset\}) y = \emptyset$
35	33 34	sylan9eq	$⊢ (φ \land (x \in S \land y \in S)) \to x J y = \emptyset$
36		rzal	$⊢ x J y = \emptyset \to \forall f \in (x J y) ψ$
37	35 36	syl	$⊢ (φ \land (x \in S \land y \in S)) \to \forall f \in (x J y) ψ$
38	37	ralrimivw	$⊢ (φ \land (x \in S \land y \in S)) \to \forall z \in S \forall f \in (x J y) ψ$
39	38	ralrimivva	$⊢ φ \to \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) ψ$
40	32 39	jca	$⊢ φ \to (\neg \forall x \in S I \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) ψ)$
41	10 22 40	jca32	$⊢ φ \to (J Fn (S \times S) \land (J \subseteq_{cat} H \land (\neg \forall x \in S I \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) ψ)))$

Metamath Proof Explorer

Theorem nelsubclem

Proof