isssc

Description: Value of the subcategory subset relation when the arguments are known functions. (Contributed by Mario Carneiro, 6-Jan-2017)

	Ref	Expression
Hypotheses	isssc.1	$⊢ φ \to H Fn (S \times S)$
	isssc.2	$⊢ φ \to J Fn (T \times T)$
	isssc.3	$⊢ φ \to T \in V$
Assertion	isssc	$⊢ φ \to (H \subseteq_{cat} J \leftrightarrow (S \subseteq T \land \forall x \in S \forall y \in S x H y \subseteq x J y))$

Proof

Step	Hyp	Ref	Expression
1		isssc.1	$⊢ φ \to H Fn (S \times S)$
2		isssc.2	$⊢ φ \to J Fn (T \times T)$
3		isssc.3	$⊢ φ \to T \in V$
4		brssc	$⊢ H \subseteq_{cat} J \leftrightarrow \exists t (J Fn (t \times t) \land \exists s \in 𝒫 t H \in \underset{z \in s \times s}{⨉} 𝒫 J (z))$
5		fndm	$⊢ J Fn (t \times t) \to dom J = t \times t$
6	5	adantl	$⊢ (φ \land J Fn (t \times t)) \to dom J = t \times t$
7	2	adantr	$⊢ (φ \land J Fn (t \times t)) \to J Fn (T \times T)$
8	7	fndmd	$⊢ (φ \land J Fn (t \times t)) \to dom J = T \times T$
9	6 8	eqtr3d	$⊢ (φ \land J Fn (t \times t)) \to t \times t = T \times T$
10	9	dmeqd	$⊢ (φ \land J Fn (t \times t)) \to dom (t \times t) = dom (T \times T)$
11		dmxpid	$⊢ dom (t \times t) = t$
12		dmxpid	$⊢ dom (T \times T) = T$
13	10 11 12	3eqtr3g	$⊢ (φ \land J Fn (t \times t)) \to t = T$
14	13	ex	$⊢ φ \to (J Fn (t \times t) \to t = T)$
15		id	$⊢ t = T \to t = T$
16	15	sqxpeqd	$⊢ t = T \to t \times t = T \times T$
17	16	fneq2d	$⊢ t = T \to (J Fn (t \times t) \leftrightarrow J Fn (T \times T))$
18	2 17	syl5ibrcom	$⊢ φ \to (t = T \to J Fn (t \times t))$
19	14 18	impbid	$⊢ φ \to (J Fn (t \times t) \leftrightarrow t = T)$
20	19	anbi1d	$⊢ φ \to ((J Fn (t \times t) \land \exists s \in 𝒫 t H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)) \leftrightarrow (t = T \land \exists s \in 𝒫 t H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)))$
21	20	exbidv	$⊢ φ \to (\exists t (J Fn (t \times t) \land \exists s \in 𝒫 t H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)) \leftrightarrow \exists t (t = T \land \exists s \in 𝒫 t H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)))$
22	4 21	bitrid	$⊢ φ \to (H \subseteq_{cat} J \leftrightarrow \exists t (t = T \land \exists s \in 𝒫 t H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)))$
23		pweq	$⊢ t = T \to 𝒫 t = 𝒫 T$
24	23	rexeqdv	$⊢ t = T \to (\exists s \in 𝒫 t H \in \underset{z \in s \times s}{⨉} 𝒫 J (z) \leftrightarrow \exists s \in 𝒫 T H \in \underset{z \in s \times s}{⨉} 𝒫 J (z))$
25	24	ceqsexgv	$⊢ T \in V \to (\exists t (t = T \land \exists s \in 𝒫 t H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)) \leftrightarrow \exists s \in 𝒫 T H \in \underset{z \in s \times s}{⨉} 𝒫 J (z))$
26	3 25	syl	$⊢ φ \to (\exists t (t = T \land \exists s \in 𝒫 t H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)) \leftrightarrow \exists s \in 𝒫 T H \in \underset{z \in s \times s}{⨉} 𝒫 J (z))$
27	22 26	bitrd	$⊢ φ \to (H \subseteq_{cat} J \leftrightarrow \exists s \in 𝒫 T H \in \underset{z \in s \times s}{⨉} 𝒫 J (z))$
28		df-rex	$⊢ \exists s \in 𝒫 T H \in \underset{z \in s \times s}{⨉} 𝒫 J (z) \leftrightarrow \exists s (s \in 𝒫 T \land H \in \underset{z \in s \times s}{⨉} 𝒫 J (z))$
29		3anass	$⊢ (H \in V \land H Fn (s \times s) \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)) \leftrightarrow (H \in V \land (H Fn (s \times s) \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)))$
30		elixp2	$⊢ H \in \underset{z \in s \times s}{⨉} 𝒫 J (z) \leftrightarrow (H \in V \land H Fn (s \times s) \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))$
31		vex	$⊢ s \in V$
32	31 31	xpex	$⊢ s \times s \in V$
33		fnex	$⊢ (H Fn (s \times s) \land s \times s \in V) \to H \in V$
34	32 33	mpan2	$⊢ H Fn (s \times s) \to H \in V$
35	34	adantr	$⊢ (H Fn (s \times s) \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)) \to H \in V$
36	35	pm4.71ri	$⊢ (H Fn (s \times s) \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)) \leftrightarrow (H \in V \land (H Fn (s \times s) \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)))$
37	29 30 36	3bitr4i	$⊢ H \in \underset{z \in s \times s}{⨉} 𝒫 J (z) \leftrightarrow (H Fn (s \times s) \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))$
38		fndm	$⊢ H Fn (s \times s) \to dom H = s \times s$
39	38	adantl	$⊢ (φ \land H Fn (s \times s)) \to dom H = s \times s$
40	1	adantr	$⊢ (φ \land H Fn (s \times s)) \to H Fn (S \times S)$
41	40	fndmd	$⊢ (φ \land H Fn (s \times s)) \to dom H = S \times S$
42	39 41	eqtr3d	$⊢ (φ \land H Fn (s \times s)) \to s \times s = S \times S$
43	42	dmeqd	$⊢ (φ \land H Fn (s \times s)) \to dom (s \times s) = dom (S \times S)$
44		dmxpid	$⊢ dom (s \times s) = s$
45		dmxpid	$⊢ dom (S \times S) = S$
46	43 44 45	3eqtr3g	$⊢ (φ \land H Fn (s \times s)) \to s = S$
47	46	ex	$⊢ φ \to (H Fn (s \times s) \to s = S)$
48		id	$⊢ s = S \to s = S$
49	48	sqxpeqd	$⊢ s = S \to s \times s = S \times S$
50	49	fneq2d	$⊢ s = S \to (H Fn (s \times s) \leftrightarrow H Fn (S \times S))$
51	1 50	syl5ibrcom	$⊢ φ \to (s = S \to H Fn (s \times s))$
52	47 51	impbid	$⊢ φ \to (H Fn (s \times s) \leftrightarrow s = S)$
53	52	anbi1d	$⊢ φ \to ((H Fn (s \times s) \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)) \leftrightarrow (s = S \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)))$
54	37 53	bitrid	$⊢ φ \to (H \in \underset{z \in s \times s}{⨉} 𝒫 J (z) \leftrightarrow (s = S \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)))$
55	54	anbi2d	$⊢ φ \to ((s \in 𝒫 T \land H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)) \leftrightarrow (s \in 𝒫 T \land (s = S \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))))$
56		an12	$⊢ (s \in 𝒫 T \land (s = S \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))) \leftrightarrow (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)))$
57	55 56	bitrdi	$⊢ φ \to ((s \in 𝒫 T \land H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)) \leftrightarrow (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))))$
58	57	exbidv	$⊢ φ \to (\exists s (s \in 𝒫 T \land H \in \underset{z \in s \times s}{⨉} 𝒫 J (z)) \leftrightarrow \exists s (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))))$
59	28 58	bitrid	$⊢ φ \to (\exists s \in 𝒫 T H \in \underset{z \in s \times s}{⨉} 𝒫 J (z) \leftrightarrow \exists s (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))))$
60		exsimpl	$⊢ \exists s (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))) \to \exists s s = S$
61		isset	$⊢ S \in V \leftrightarrow \exists s s = S$
62	60 61	sylibr	$⊢ \exists s (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))) \to S \in V$
63	62	a1i	$⊢ φ \to (\exists s (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))) \to S \in V)$
64		ssexg	$⊢ (S \subseteq T \land T \in V) \to S \in V$
65	64	expcom	$⊢ T \in V \to (S \subseteq T \to S \in V)$
66	3 65	syl	$⊢ φ \to (S \subseteq T \to S \in V)$
67	66	adantrd	$⊢ φ \to ((S \subseteq T \land \forall x \in S \forall y \in S x H y \subseteq x J y) \to S \in V)$
68	31	elpw	$⊢ s \in 𝒫 T \leftrightarrow s \subseteq T$
69		sseq1	$⊢ s = S \to (s \subseteq T \leftrightarrow S \subseteq T)$
70	68 69	bitrid	$⊢ s = S \to (s \in 𝒫 T \leftrightarrow S \subseteq T)$
71	49	raleqdv	$⊢ s = S \to (\forall z \in (s \times s) H (z) \in 𝒫 J (z) \leftrightarrow \forall z \in (S \times S) H (z) \in 𝒫 J (z))$
72		fvex	$⊢ H (z) \in V$
73	72	elpw	$⊢ H (z) \in 𝒫 J (z) \leftrightarrow H (z) \subseteq J (z)$
74		fveq2	$⊢ z = ⟨x, y⟩ \to H (z) = H (⟨x, y⟩)$
75		df-ov	$⊢ x H y = H (⟨x, y⟩)$
76	74 75	eqtr4di	$⊢ z = ⟨x, y⟩ \to H (z) = x H y$
77		fveq2	$⊢ z = ⟨x, y⟩ \to J (z) = J (⟨x, y⟩)$
78		df-ov	$⊢ x J y = J (⟨x, y⟩)$
79	77 78	eqtr4di	$⊢ z = ⟨x, y⟩ \to J (z) = x J y$
80	76 79	sseq12d	$⊢ z = ⟨x, y⟩ \to (H (z) \subseteq J (z) \leftrightarrow x H y \subseteq x J y)$
81	73 80	bitrid	$⊢ z = ⟨x, y⟩ \to (H (z) \in 𝒫 J (z) \leftrightarrow x H y \subseteq x J y)$
82	81	ralxp	$⊢ \forall z \in (S \times S) H (z) \in 𝒫 J (z) \leftrightarrow \forall x \in S \forall y \in S x H y \subseteq x J y$
83	71 82	bitrdi	$⊢ s = S \to (\forall z \in (s \times s) H (z) \in 𝒫 J (z) \leftrightarrow \forall x \in S \forall y \in S x H y \subseteq x J y)$
84	70 83	anbi12d	$⊢ s = S \to ((s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z)) \leftrightarrow (S \subseteq T \land \forall x \in S \forall y \in S x H y \subseteq x J y))$
85	84	ceqsexgv	$⊢ S \in V \to (\exists s (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))) \leftrightarrow (S \subseteq T \land \forall x \in S \forall y \in S x H y \subseteq x J y))$
86	85	a1i	$⊢ φ \to (S \in V \to (\exists s (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))) \leftrightarrow (S \subseteq T \land \forall x \in S \forall y \in S x H y \subseteq x J y)))$
87	63 67 86	pm5.21ndd	$⊢ φ \to (\exists s (s = S \land (s \in 𝒫 T \land \forall z \in (s \times s) H (z) \in 𝒫 J (z))) \leftrightarrow (S \subseteq T \land \forall x \in S \forall y \in S x H y \subseteq x J y))$
88	27 59 87	3bitrd	$⊢ φ \to (H \subseteq_{cat} J \leftrightarrow (S \subseteq T \land \forall x \in S \forall y \in S x H y \subseteq x J y))$

Metamath Proof Explorer

Theorem isssc

Proof