nelsubc3lem

	Ref	Expression
Hypotheses	nelsubc3lem.c	$⊢ C \in Cat$
	nelsubc3lem.j	$⊢ J \in V$
	nelsubc3lem.s	$⊢ S \in V$
	nelsubc3lem.1	$⊢ (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 \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))))$
Assertion	nelsubc3lem	$⊢ \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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z))))$

Proof

Step	Hyp	Ref	Expression
1		nelsubc3lem.c	$⊢ C \in Cat$
2		nelsubc3lem.j	$⊢ J \in V$
3		nelsubc3lem.s	$⊢ S \in V$
4		nelsubc3lem.1	$⊢ (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 \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))))$
5		id	$⊢ s = S \to s = S$
6	5	sqxpeqd	$⊢ s = S \to s \times s = S \times S$
7	6	fneq2d	$⊢ s = S \to (J Fn (s \times s) \leftrightarrow J Fn (S \times S))$
8		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))$
9	8	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))$
10		raleq	$⊢ s = S \to (\forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z) \leftrightarrow \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
11	10	raleqbi1dv	$⊢ s = S \to (\forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z) \leftrightarrow \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
12	11	raleqbi1dv	$⊢ s = S \to (\forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z) \leftrightarrow \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
13	9 12	anbi12d	$⊢ s = S \to ((\neg \forall x \in s Id (C) (x) \in (x J x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)) \leftrightarrow (\neg \forall x \in S Id (C) (x) \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)))$
14	13	anbi2d	$⊢ s = S \to ((J \subseteq_{cat} {Hom}_{𝑓} (C) \land (\neg \forall x \in s Id (C) (x) \in (x J x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (C) \land (\neg \forall x \in S Id (C) (x) \in (x J x) \land \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))))$
15	7 14	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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)))) \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 \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)))))$
16	3 15	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 \forall x \in S \forall y \in S \forall z \in S \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)))) \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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))))$
17		fneq1	$⊢ j = J \to (j Fn (s \times s) \leftrightarrow J Fn (s \times s))$
18		breq1	$⊢ j = J \to (j \subseteq_{cat} {Hom}_{𝑓} (C) \leftrightarrow J \subseteq_{cat} {Hom}_{𝑓} (C))$
19		oveq	$⊢ j = J \to x j x = x J x$
20	19	eleq2d	$⊢ j = J \to (Id (C) (x) \in (x j x) \leftrightarrow Id (C) (x) \in (x J x))$
21	20	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))$
22	21	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))$
23		oveq	$⊢ j = J \to x j y = x J y$
24		oveq	$⊢ j = J \to y j z = y J z$
25		oveq	$⊢ j = J \to x j z = x J z$
26	25	eleq2d	$⊢ j = J \to (g (⟨x, y⟩ comp (C) z) f \in (x j z) \leftrightarrow g (⟨x, y⟩ comp (C) z) f \in (x J z))$
27	24 26	raleqbidv	$⊢ j = J \to (\forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z) \leftrightarrow \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
28	23 27	raleqbidv	$⊢ j = J \to (\forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z) \leftrightarrow \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
29	28	3ralbidv	$⊢ j = J \to (\forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z) \leftrightarrow \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))$
30	22 29	anbi12d	$⊢ j = J \to ((\neg \forall x \in s Id (C) (x) \in (x j x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z)) \leftrightarrow (\neg \forall x \in s Id (C) (x) \in (x J x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)))$
31	18 30	anbi12d	$⊢ j = J \to ((j \subseteq_{cat} {Hom}_{𝑓} (C) \land (\neg \forall x \in s Id (C) (x) \in (x j x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z))) \leftrightarrow (J \subseteq_{cat} {Hom}_{𝑓} (C) \land (\neg \forall x \in s Id (C) (x) \in (x J x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z))))$
32	17 31	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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z)))) \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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)))))$
33	32	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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z)))) \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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)))))$
34	2 33	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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x J y) \forall g \in (y J z) g (⟨x, y⟩ comp (C) z) f \in (x J z)))) \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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z))))$
35	4 16 34	mp2b	$⊢ \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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z))))$
36		fveq2	$⊢ c = C \to {Hom}_{𝑓} (c) = {Hom}_{𝑓} (C)$
37	36	breq2d	$⊢ c = C \to (j \subseteq_{cat} {Hom}_{𝑓} (c) \leftrightarrow j \subseteq_{cat} {Hom}_{𝑓} (C))$
38		fveq2	$⊢ c = C \to Id (c) = Id (C)$
39	38	fveq1d	$⊢ c = C \to Id (c) (x) = Id (C) (x)$
40	39	eleq1d	$⊢ c = C \to (Id (c) (x) \in (x j x) \leftrightarrow Id (C) (x) \in (x j x))$
41	40	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))$
42	41	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))$
43		fveq2	$⊢ c = C \to comp (c) = comp (C)$
44	43	oveqd	$⊢ c = C \to ⟨x, y⟩ comp (c) z = ⟨x, y⟩ comp (C) z$
45	44	oveqd	$⊢ c = C \to g (⟨x, y⟩ comp (c) z) f = g (⟨x, y⟩ comp (C) z) f$
46	45	eleq1d	$⊢ c = C \to (g (⟨x, y⟩ comp (c) z) f \in (x j z) \leftrightarrow g (⟨x, y⟩ comp (C) z) f \in (x j z))$
47	46	ralbidv	$⊢ c = C \to (\forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z) \leftrightarrow \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z))$
48	47	4ralbidv	$⊢ c = C \to (\forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z) \leftrightarrow \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z))$
49	42 48	anbi12d	$⊢ c = C \to ((\neg \forall x \in s Id (c) (x) \in (x j x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z)) \leftrightarrow (\neg \forall x \in s Id (C) (x) \in (x j x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z)))$
50	37 49	anbi12d	$⊢ c = C \to ((j \subseteq_{cat} {Hom}_{𝑓} (c) \land (\neg \forall x \in s Id (c) (x) \in (x j x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z))) \leftrightarrow (j \subseteq_{cat} {Hom}_{𝑓} (C) \land (\neg \forall x \in s Id (C) (x) \in (x j x) \land \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z))))$
51	50	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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z)))) \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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z)))))$
52	51	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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z)))) \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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z)))))$
53	52	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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (C) z) f \in (x j z))))) \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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z))))$
54	1 35 53	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 \forall x \in s \forall y \in s \forall z \in s \forall f \in (x j y) \forall g \in (y j z) g (⟨x, y⟩ comp (c) z) f \in (x j z))))$

Metamath Proof Explorer

Theorem nelsubc3lem

Proof