cnelsubclem

	Ref	Expression
Hypotheses	cnelsubclem.1	$⊢ J \in V$
	cnelsubclem.2	$⊢ S \in V$
	cnelsubclem.3	$⊢ (C \in Cat \land J Fn (S \times S) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in S Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat))$
Assertion	cnelsubclem	$⊢ \exists c \in Cat \exists j \exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \neg \forall x \in s Id (c) (x) \in (x j x) \land c ↾_{cat} j \in Cat))$

Proof

Step	Hyp	Ref	Expression
1		cnelsubclem.1	$⊢ J \in V$
2		cnelsubclem.2	$⊢ S \in V$
3		cnelsubclem.3	$⊢ (C \in Cat \land J Fn (S \times S) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in S Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat))$
4	3	simp1i	$⊢ C \in Cat$
5	3	simp2i	$⊢ J Fn (S \times S)$
6	3	simp3i	$⊢ (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in S Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat)$
7		id	$⊢ s = S \to s = S$
8	7	sqxpeqd	$⊢ s = S \to s \times s = S \times S$
9	8	fneq2d	$⊢ s = S \to (J Fn (s \times s) \leftrightarrow J Fn (S \times S))$
10		raleq	$⊢ s = S \to (\forall x \in s Id (C) (x) \in (x J x) \leftrightarrow \forall x \in S Id (C) (x) \in (x J x))$
11	10	notbid	$⊢ s = S \to (\neg \forall x \in s Id (C) (x) \in (x J x) \leftrightarrow \neg \forall x \in S Id (C) (x) \in (x J x))$
12	11	3anbi2d	$⊢ s = S \to ((J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in S Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat))$
13	9 12	anbi12d	$⊢ s = S \to ((J Fn (s \times s) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat)) \leftrightarrow (J Fn (S \times S) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in S Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat)))$
14	2 13	spcev	$⊢ (J Fn (S \times S) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in S Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat)) \to \exists s (J Fn (s \times s) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat))$
15		fneq1	$⊢ j = J \to (j Fn (s \times s) \leftrightarrow J Fn (s \times s))$
16		breq1	$⊢ j = J \to (j \subseteq_{cat} {Hom}_{𝑓} (C) \leftrightarrow J \subseteq_{cat} {Hom}_{𝑓} (C))$
17		oveq	$⊢ j = J \to x j x = x J x$
18	17	eleq2d	$⊢ j = J \to (Id (C) (x) \in (x j x) \leftrightarrow Id (C) (x) \in (x J x))$
19	18	ralbidv	$⊢ j = J \to (\forall x \in s Id (C) (x) \in (x j x) \leftrightarrow \forall x \in s Id (C) (x) \in (x J x))$
20	19	notbid	$⊢ j = J \to (\neg \forall x \in s Id (C) (x) \in (x j x) \leftrightarrow \neg \forall x \in s Id (C) (x) \in (x J x))$
21		oveq2	$⊢ j = J \to C ↾_{cat} j = C ↾_{cat} J$
22	21	eleq1d	$⊢ j = J \to (C ↾_{cat} j \in Cat \leftrightarrow C ↾_{cat} J \in Cat)$
23	16 20 22	3anbi123d	$⊢ j = J \to ((j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat))$
24	15 23	anbi12d	$⊢ j = J \to ((j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat)) \leftrightarrow (J Fn (s \times s) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat)))$
25	24	exbidv	$⊢ j = J \to (\exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat)) \leftrightarrow \exists s (J Fn (s \times s) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat)))$
26	1 25	spcev	$⊢ \exists s (J Fn (s \times s) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat)) \to \exists j \exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat))$
27	14 26	syl	$⊢ (J Fn (S \times S) \land (J \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in S Id (C) (x) \in (x J x) \land C ↾_{cat} J \in Cat)) \to \exists j \exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat))$
28	5 6 27	mp2an	$⊢ \exists j \exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat))$
29		fveq2	$⊢ c = C \to {Hom}_{𝑓} (c) = {Hom}_{𝑓} (C)$
30	29	breq2d	$⊢ c = C \to (j \subseteq_{cat} {Hom}_{𝑓} (c) \leftrightarrow j \subseteq_{cat} {Hom}_{𝑓} (C))$
31		fveq2	$⊢ c = C \to Id (c) = Id (C)$
32	31	fveq1d	$⊢ c = C \to Id (c) (x) = Id (C) (x)$
33	32	eleq1d	$⊢ c = C \to (Id (c) (x) \in (x j x) \leftrightarrow Id (C) (x) \in (x j x))$
34	33	ralbidv	$⊢ c = C \to (\forall x \in s Id (c) (x) \in (x j x) \leftrightarrow \forall x \in s Id (C) (x) \in (x j x))$
35	34	notbid	$⊢ c = C \to (\neg \forall x \in s Id (c) (x) \in (x j x) \leftrightarrow \neg \forall x \in s Id (C) (x) \in (x j x))$
36		oveq1	$⊢ c = C \to c ↾_{cat} j = C ↾_{cat} j$
37	36	eleq1d	$⊢ c = C \to (c ↾_{cat} j \in Cat \leftrightarrow C ↾_{cat} j \in Cat)$
38	30 35 37	3anbi123d	$⊢ c = C \to ((j \subseteq_{cat} {Hom}_{𝑓} (c) \land \neg \forall x \in s Id (c) (x) \in (x j x) \land c ↾_{cat} j \in Cat) \leftrightarrow (j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat))$
39	38	anbi2d	$⊢ c = C \to ((j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \neg \forall x \in s Id (c) (x) \in (x j x) \land c ↾_{cat} j \in Cat)) \leftrightarrow (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat)))$
40	39	2exbidv	$⊢ c = C \to (\exists j \exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \neg \forall x \in s Id (c) (x) \in (x j x) \land c ↾_{cat} j \in Cat)) \leftrightarrow \exists j \exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat)))$
41	40	rspcev	$⊢ (C \in Cat \land \exists j \exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (C) \land \neg \forall x \in s Id (C) (x) \in (x j x) \land C ↾_{cat} j \in Cat))) \to \exists c \in Cat \exists j \exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \neg \forall x \in s Id (c) (x) \in (x j x) \land c ↾_{cat} j \in Cat))$
42	4 28 41	mp2an	$⊢ \exists c \in Cat \exists j \exists s (j Fn (s \times s) \land (j \subseteq_{cat} {Hom}_{𝑓} (c) \land \neg \forall x \in s Id (c) (x) \in (x j x) \land c ↾_{cat} j \in Cat))$

Metamath Proof Explorer

Theorem cnelsubclem

Proof