Theorem isssc 17727

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

Hypotheses

Ref	Expression
isssc.1	⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
isssc.2	⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))
isssc.3	⊢ (𝜑 → 𝑇 ∈ 𝑉)

Assertion

Ref	Expression
isssc	⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))

Distinct variable groups:   𝑥,𝑦,𝐻   𝑥,𝐽,𝑦   𝑥,𝑆,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝑇(𝑥,𝑦)   𝑉(𝑥,𝑦)

Proof of Theorem isssc

Dummy variables 𝑡 𝑠 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		brssc 17721	. . . 4 ⊢ (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))
2		fndm 6584	. . . . . . . . . . . 12 ⊢ (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡))
3	2	adantl 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑡 × 𝑡))
4		isssc.2	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐽 Fn (𝑇 × 𝑇))
5	4	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝐽 Fn (𝑇 × 𝑇))
6	5	fndmd 6586	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑇 × 𝑇))
7	3, 6	eqtr3d 2768	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → (𝑡 × 𝑡) = (𝑇 × 𝑇))
8	7	dmeqd 5844	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → dom (𝑡 × 𝑡) = dom (𝑇 × 𝑇))
9		dmxpid 5869	. . . . . . . . 9 ⊢ dom (𝑡 × 𝑡) = 𝑡
10		dmxpid 5869	. . . . . . . . 9 ⊢ dom (𝑇 × 𝑇) = 𝑇
11	8, 9, 10	3eqtr3g 2789	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐽 Fn (𝑡 × 𝑡)) → 𝑡 = 𝑇)
12	11	ex 412	. . . . . . 7 ⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) → 𝑡 = 𝑇))
13		id 22	. . . . . . . . . 10 ⊢ (𝑡 = 𝑇 → 𝑡 = 𝑇)
14	13	sqxpeqd 5646	. . . . . . . . 9 ⊢ (𝑡 = 𝑇 → (𝑡 × 𝑡) = (𝑇 × 𝑇))
15	14	fneq2d 6575	. . . . . . . 8 ⊢ (𝑡 = 𝑇 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑇 × 𝑇)))
16	4, 15	syl5ibrcom 247	. . . . . . 7 ⊢ (𝜑 → (𝑡 = 𝑇 → 𝐽 Fn (𝑡 × 𝑡)))
17	12, 16	impbid 212	. . . . . 6 ⊢ (𝜑 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝑡 = 𝑇))
18	17	anbi1d 631	. . . . 5 ⊢ (𝜑 → ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))))
19	18	exbidv 1922	. . . 4 ⊢ (𝜑 → (∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))))
20	1, 19	bitrid 283	. . 3 ⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧))))
21		isssc.3	. . . 4 ⊢ (𝜑 → 𝑇 ∈ 𝑉)
22		pweq 4561	. . . . . 6 ⊢ (𝑡 = 𝑇 → 𝒫 𝑡 = 𝒫 𝑇)
23	22	rexeqdv 3293	. . . . 5 ⊢ (𝑡 = 𝑇 → (∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))
24	23	ceqsexgv 3604	. . . 4 ⊢ (𝑇 ∈ 𝑉 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))
25	21, 24	syl 17	. . 3 ⊢ (𝜑 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))
26	20, 25	bitrd 279	. 2 ⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))
27		df-rex 3057	. . 3 ⊢ (∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)))
28		3anass 1094	. . . . . . . 8 ⊢ ((𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))
29		elixp2 8825	. . . . . . . 8 ⊢ (𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))
30		vex 3440	. . . . . . . . . . . 12 ⊢ 𝑠 ∈ V
31	30, 30	xpex 7686	. . . . . . . . . . 11 ⊢ (𝑠 × 𝑠) ∈ V
32		fnex 7151	. . . . . . . . . . 11 ⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ (𝑠 × 𝑠) ∈ V) → 𝐻 ∈ V)
33	31, 32	mpan2 691	. . . . . . . . . 10 ⊢ (𝐻 Fn (𝑠 × 𝑠) → 𝐻 ∈ V)
34	33	adantr 480	. . . . . . . . 9 ⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) → 𝐻 ∈ V)
35	34	pm4.71ri 560	. . . . . . . 8 ⊢ ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))
36	28, 29, 35	3bitr4i 303	. . . . . . 7 ⊢ (𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))
37		fndm 6584	. . . . . . . . . . . . . 14 ⊢ (𝐻 Fn (𝑠 × 𝑠) → dom 𝐻 = (𝑠 × 𝑠))
38	37	adantl 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑠 × 𝑠))
39		isssc.1	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐻 Fn (𝑆 × 𝑆))
40	39	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝐻 Fn (𝑆 × 𝑆))
41	40	fndmd 6586	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑆 × 𝑆))
42	38, 41	eqtr3d 2768	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → (𝑠 × 𝑠) = (𝑆 × 𝑆))
43	42	dmeqd 5844	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → dom (𝑠 × 𝑠) = dom (𝑆 × 𝑆))
44		dmxpid 5869	. . . . . . . . . . 11 ⊢ dom (𝑠 × 𝑠) = 𝑠
45		dmxpid 5869	. . . . . . . . . . 11 ⊢ dom (𝑆 × 𝑆) = 𝑆
46	43, 44, 45	3eqtr3g 2789	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐻 Fn (𝑠 × 𝑠)) → 𝑠 = 𝑆)
47	46	ex 412	. . . . . . . . 9 ⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) → 𝑠 = 𝑆))
48		id 22	. . . . . . . . . . . 12 ⊢ (𝑠 = 𝑆 → 𝑠 = 𝑆)
49	48	sqxpeqd 5646	. . . . . . . . . . 11 ⊢ (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆))
50	49	fneq2d 6575	. . . . . . . . . 10 ⊢ (𝑠 = 𝑆 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝐻 Fn (𝑆 × 𝑆)))
51	39, 50	syl5ibrcom 247	. . . . . . . . 9 ⊢ (𝜑 → (𝑠 = 𝑆 → 𝐻 Fn (𝑠 × 𝑠)))
52	47, 51	impbid 212	. . . . . . . 8 ⊢ (𝜑 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝑠 = 𝑆))
53	52	anbi1d 631	. . . . . . 7 ⊢ (𝜑 → ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))
54	36, 53	bitrid 283	. . . . . 6 ⊢ (𝜑 → (𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))
55	54	anbi2d 630	. . . . 5 ⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))))
56		an12 645	. . . . 5 ⊢ ((𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))))
57	55, 56	bitrdi 287	. . . 4 ⊢ (𝜑 → ((𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))))
58	57	exbidv 1922	. . 3 ⊢ (𝜑 → (∃𝑠(𝑠 ∈ 𝒫 𝑇 ∧ 𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧)) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))))
59	27, 58	bitrid 283	. 2 ⊢ (𝜑 → (∃𝑠 ∈ 𝒫 𝑇𝐻 ∈ X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽‘𝑧) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))))
60		exsimpl 1869	. . . . 5 ⊢ (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → ∃𝑠 𝑠 = 𝑆)
61		isset 3450	. . . . 5 ⊢ (𝑆 ∈ V ↔ ∃𝑠 𝑠 = 𝑆)
62	60, 61	sylibr 234	. . . 4 ⊢ (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V)
63	62	a1i 11	. . 3 ⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) → 𝑆 ∈ V))
64		ssexg 5259	. . . . . 6 ⊢ ((𝑆 ⊆ 𝑇 ∧ 𝑇 ∈ 𝑉) → 𝑆 ∈ V)
65	64	expcom 413	. . . . 5 ⊢ (𝑇 ∈ 𝑉 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V))
66	21, 65	syl 17	. . . 4 ⊢ (𝜑 → (𝑆 ⊆ 𝑇 → 𝑆 ∈ V))
67	66	adantrd 491	. . 3 ⊢ (𝜑 → ((𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) → 𝑆 ∈ V))
68	30	elpw 4551	. . . . . . 7 ⊢ (𝑠 ∈ 𝒫 𝑇 ↔ 𝑠 ⊆ 𝑇)
69		sseq1 3955	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (𝑠 ⊆ 𝑇 ↔ 𝑆 ⊆ 𝑇))
70	68, 69	bitrid 283	. . . . . 6 ⊢ (𝑠 = 𝑆 → (𝑠 ∈ 𝒫 𝑇 ↔ 𝑆 ⊆ 𝑇))
71	49	raleqdv 3292	. . . . . . 7 ⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)))
72		fvex 6835	. . . . . . . . . 10 ⊢ (𝐻‘𝑧) ∈ V
73	72	elpw 4551	. . . . . . . . 9 ⊢ ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝐻‘𝑧) ⊆ (𝐽‘𝑧))
74		fveq2 6822	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻‘𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
75		df-ov 7349	. . . . . . . . . . 11 ⊢ (𝑥𝐻𝑦) = (𝐻‘⟨𝑥, 𝑦⟩)
76	74, 75	eqtr4di 2784	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻‘𝑧) = (𝑥𝐻𝑦))
77		fveq2 6822	. . . . . . . . . . 11 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐽‘𝑧) = (𝐽‘⟨𝑥, 𝑦⟩))
78		df-ov 7349	. . . . . . . . . . 11 ⊢ (𝑥𝐽𝑦) = (𝐽‘⟨𝑥, 𝑦⟩)
79	77, 78	eqtr4di 2784	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐽‘𝑧) = (𝑥𝐽𝑦))
80	76, 79	sseq12d 3963	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻‘𝑧) ⊆ (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
81	73, 80	bitrid 283	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
82	81	ralxp 5780	. . . . . . 7 ⊢ (∀𝑧 ∈ (𝑆 × 𝑆)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))
83	71, 82	bitrdi 287	. . . . . 6 ⊢ (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧) ↔ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
84	70, 83	anbi12d 632	. . . . 5 ⊢ (𝑠 = 𝑆 → ((𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧)) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
85	84	ceqsexgv 3604	. . . 4 ⊢ (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
86	85	a1i 11	. . 3 ⊢ (𝜑 → (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))))
87	63, 67, 86	pm5.21ndd 379	. 2 ⊢ (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻‘𝑧) ∈ 𝒫 (𝐽‘𝑧))) ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
88	26, 59, 87	3bitrd 305	1 ⊢ (𝜑 → (𝐻 ⊆cat 𝐽 ↔ (𝑆 ⊆ 𝑇 ∧ ∀𝑥 ∈ 𝑆 ∀𝑦 ∈ 𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541  ∃wex 1780   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056  Vcvv 3436   ⊆ wss 3897  𝒫 cpw 4547  ⟨cop 4579   class class class wbr 5089   × cxp 5612  dom cdm 5614   Fn wfn 6476  ‘cfv 6481  (class class class)co 7346  Xcixp 8821   ⊆_cat cssc 17714

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5215  ax-sep 5232  ax-nul 5242  ax-pow 5301  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-pw 4549  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-iun 4941  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fo 6487  df-f1o 6488  df-fv 6489  df-ov 7349  df-ixp 8822  df-ssc 17717

This theorem is referenced by:  ssc1  17728  ssc2  17729  sscres  17730  ssctr  17732  0ssc  17744  catsubcat  17746  rnghmsscmap2  20544  rnghmsscmap  20545  rhmsscmap2  20573  rhmsscmap  20574  rhmsscrnghm  20580  srhmsubc  20595  fldhmsubc  20700  srhmsubcALTV  48435  fldhmsubcALTV  48443  iinfssc  49168  discsubc  49175  nelsubclem  49178  imassc  49264  setc1onsubc  49713