MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  issubc Structured version   Visualization version   GIF version

Theorem issubc 16808
Description: Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
issubc.h 𝐻 = (Homf𝐶)
issubc.i 1 = (Id‘𝐶)
issubc.o · = (comp‘𝐶)
issubc.c (𝜑𝐶 ∈ Cat)
issubc.s (𝜑𝑆 = dom dom 𝐽)
Assertion
Ref Expression
issubc (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
Distinct variable groups:   𝑓,𝑔,𝑥,𝑦,𝑧,𝐶   𝑓,𝐽,𝑔,𝑥,𝑦,𝑧   𝑆,𝑓,𝑔,𝑥,𝑦,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑓,𝑔)   · (𝑥,𝑦,𝑧,𝑓,𝑔)   1 (𝑥,𝑦,𝑧,𝑓,𝑔)   𝐻(𝑥,𝑦,𝑧,𝑓,𝑔)

Proof of Theorem issubc
Dummy variables 𝑐 𝑗 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 issubc.c . 2 (𝜑𝐶 ∈ Cat)
2 issubc.s . 2 (𝜑𝑆 = dom dom 𝐽)
3 simpl 475 . . . . 5 ((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) → 𝐶 ∈ Cat)
4 sscpwex 16788 . . . . . . . 8 {𝑗𝑗cat (Homf𝑐)} ∈ V
5 simpl 475 . . . . . . . . 9 ((𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧))) → 𝑗cat (Homf𝑐))
65ss2abi 3871 . . . . . . . 8 {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ⊆ {𝑗𝑗cat (Homf𝑐)}
74, 6ssexi 4999 . . . . . . 7 {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ∈ V
87csbex 4989 . . . . . 6 𝐶 / 𝑐{𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ∈ V
98a1i 11 . . . . 5 ((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) → 𝐶 / 𝑐{𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ∈ V)
10 df-subc 16785 . . . . . 6 Subcat = (𝑐 ∈ Cat ↦ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))})
1110fvmpts 6511 . . . . 5 ((𝐶 ∈ Cat ∧ 𝐶 / 𝑐{𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ∈ V) → (Subcat‘𝐶) = 𝐶 / 𝑐{𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))})
123, 9, 11syl2anc 580 . . . 4 ((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) → (Subcat‘𝐶) = 𝐶 / 𝑐{𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))})
1312eleq2d 2865 . . 3 ((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) → (𝐽 ∈ (Subcat‘𝐶) ↔ 𝐽𝐶 / 𝑐{𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))}))
14 sbcel2 4185 . . . 4 ([𝐶 / 𝑐]𝐽 ∈ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ↔ 𝐽𝐶 / 𝑐{𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))})
1514a1i 11 . . 3 ((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) → ([𝐶 / 𝑐]𝐽 ∈ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ↔ 𝐽𝐶 / 𝑐{𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))}))
16 elex 3401 . . . . . 6 (𝐽 ∈ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} → 𝐽 ∈ V)
1716a1i 11 . . . . 5 (((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) → (𝐽 ∈ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} → 𝐽 ∈ V))
18 sscrel 16786 . . . . . . . 8 Rel ⊆cat
1918brrelex1i 5364 . . . . . . 7 (𝐽cat 𝐻𝐽 ∈ V)
2019adantr 473 . . . . . 6 ((𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧))) → 𝐽 ∈ V)
2120a1i 11 . . . . 5 (((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) → ((𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧))) → 𝐽 ∈ V))
22 df-sbc 3635 . . . . . . 7 ([𝐽 / 𝑗](𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧))) ↔ 𝐽 ∈ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))})
23 simpr 478 . . . . . . . 8 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝐽 ∈ V) → 𝐽 ∈ V)
24 simpr 478 . . . . . . . . . . 11 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → 𝑗 = 𝐽)
25 simpr 478 . . . . . . . . . . . . . 14 (((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) → 𝑐 = 𝐶)
2625fveq2d 6416 . . . . . . . . . . . . 13 (((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) → (Homf𝑐) = (Homf𝐶))
27 issubc.h . . . . . . . . . . . . 13 𝐻 = (Homf𝐶)
2826, 27syl6eqr 2852 . . . . . . . . . . . 12 (((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) → (Homf𝑐) = 𝐻)
2928adantr 473 . . . . . . . . . . 11 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → (Homf𝑐) = 𝐻)
3024, 29breq12d 4857 . . . . . . . . . 10 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → (𝑗cat (Homf𝑐) ↔ 𝐽cat 𝐻))
31 vex 3389 . . . . . . . . . . . . . 14 𝑗 ∈ V
3231dmex 7335 . . . . . . . . . . . . 13 dom 𝑗 ∈ V
3332dmex 7335 . . . . . . . . . . . 12 dom dom 𝑗 ∈ V
3433a1i 11 . . . . . . . . . . 11 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → dom dom 𝑗 ∈ V)
3524dmeqd 5530 . . . . . . . . . . . . 13 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → dom 𝑗 = dom 𝐽)
3635dmeqd 5530 . . . . . . . . . . . 12 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → dom dom 𝑗 = dom dom 𝐽)
37 simpllr 794 . . . . . . . . . . . 12 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → 𝑆 = dom dom 𝐽)
3836, 37eqtr4d 2837 . . . . . . . . . . 11 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → dom dom 𝑗 = 𝑆)
39 simpr 478 . . . . . . . . . . . 12 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆)
40 simpllr 794 . . . . . . . . . . . . . . . . 17 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → 𝑐 = 𝐶)
4140fveq2d 6416 . . . . . . . . . . . . . . . 16 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (Id‘𝑐) = (Id‘𝐶))
42 issubc.i . . . . . . . . . . . . . . . 16 1 = (Id‘𝐶)
4341, 42syl6eqr 2852 . . . . . . . . . . . . . . 15 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (Id‘𝑐) = 1 )
4443fveq1d 6414 . . . . . . . . . . . . . 14 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → ((Id‘𝑐)‘𝑥) = ( 1𝑥))
45 simplr 786 . . . . . . . . . . . . . . 15 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → 𝑗 = 𝐽)
4645oveqd 6896 . . . . . . . . . . . . . 14 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (𝑥𝑗𝑥) = (𝑥𝐽𝑥))
4744, 46eleq12d 2873 . . . . . . . . . . . . 13 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ↔ ( 1𝑥) ∈ (𝑥𝐽𝑥)))
4845oveqd 6896 . . . . . . . . . . . . . . . 16 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (𝑥𝑗𝑦) = (𝑥𝐽𝑦))
4945oveqd 6896 . . . . . . . . . . . . . . . . 17 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (𝑦𝑗𝑧) = (𝑦𝐽𝑧))
5040fveq2d 6416 . . . . . . . . . . . . . . . . . . . . 21 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (comp‘𝑐) = (comp‘𝐶))
51 issubc.o . . . . . . . . . . . . . . . . . . . . 21 · = (comp‘𝐶)
5250, 51syl6eqr 2852 . . . . . . . . . . . . . . . . . . . 20 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (comp‘𝑐) = · )
5352oveqd 6896 . . . . . . . . . . . . . . . . . . 19 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧) = (⟨𝑥, 𝑦· 𝑧))
5453oveqd 6896 . . . . . . . . . . . . . . . . . 18 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) = (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓))
5545oveqd 6896 . . . . . . . . . . . . . . . . . 18 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (𝑥𝑗𝑧) = (𝑥𝐽𝑧))
5654, 55eleq12d 2873 . . . . . . . . . . . . . . . . 17 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → ((𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ (𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
5749, 56raleqbidv 3336 . . . . . . . . . . . . . . . 16 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ ∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
5848, 57raleqbidv 3336 . . . . . . . . . . . . . . 15 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (∀𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ ∀𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
5939, 58raleqbidv 3336 . . . . . . . . . . . . . 14 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (∀𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ ∀𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
6039, 59raleqbidv 3336 . . . . . . . . . . . . 13 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧) ↔ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))
6147, 60anbi12d 625 . . . . . . . . . . . 12 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → ((((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)) ↔ (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))
6239, 61raleqbidv 3336 . . . . . . . . . . 11 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) ∧ 𝑠 = 𝑆) → (∀𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)) ↔ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))
6334, 38, 62sbcied2 3672 . . . . . . . . . 10 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → ([dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)) ↔ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))
6430, 63anbi12d 625 . . . . . . . . 9 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝑗 = 𝐽) → ((𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧))) ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
6564adantlr 707 . . . . . . . 8 (((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝐽 ∈ V) ∧ 𝑗 = 𝐽) → ((𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧))) ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
6623, 65sbcied 3671 . . . . . . 7 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝐽 ∈ V) → ([𝐽 / 𝑗](𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧))) ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
6722, 66syl5bbr 277 . . . . . 6 ((((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) ∧ 𝐽 ∈ V) → (𝐽 ∈ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
6867ex 402 . . . . 5 (((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) → (𝐽 ∈ V → (𝐽 ∈ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧))))))
6917, 21, 68pm5.21ndd 371 . . . 4 (((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) ∧ 𝑐 = 𝐶) → (𝐽 ∈ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
703, 69sbcied 3671 . . 3 ((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) → ([𝐶 / 𝑐]𝐽 ∈ {𝑗 ∣ (𝑗cat (Homf𝑐) ∧ [dom dom 𝑗 / 𝑠]𝑥𝑠 (((Id‘𝑐)‘𝑥) ∈ (𝑥𝑗𝑥) ∧ ∀𝑦𝑠𝑧𝑠𝑓 ∈ (𝑥𝑗𝑦)∀𝑔 ∈ (𝑦𝑗𝑧)(𝑔(⟨𝑥, 𝑦⟩(comp‘𝑐)𝑧)𝑓) ∈ (𝑥𝑗𝑧)))} ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
7113, 15, 703bitr2d 299 . 2 ((𝐶 ∈ Cat ∧ 𝑆 = dom dom 𝐽) → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
721, 2, 71syl2anc 580 1 (𝜑 → (𝐽 ∈ (Subcat‘𝐶) ↔ (𝐽cat 𝐻 ∧ ∀𝑥𝑆 (( 1𝑥) ∈ (𝑥𝐽𝑥) ∧ ∀𝑦𝑆𝑧𝑆𝑓 ∈ (𝑥𝐽𝑦)∀𝑔 ∈ (𝑦𝐽𝑧)(𝑔(⟨𝑥, 𝑦· 𝑧)𝑓) ∈ (𝑥𝐽𝑧)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 385   = wceq 1653  wcel 2157  {cab 2786  wral 3090  Vcvv 3386  [wsbc 3634  csb 3729  cop 4375   class class class wbr 4844  dom cdm 5313  cfv 6102  (class class class)co 6879  compcco 16278  Catccat 16638  Idccid 16639  Homf chomf 16640  cat cssc 16780  Subcatcsubc 16782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-8 2159  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-rep 4965  ax-sep 4976  ax-nul 4984  ax-pow 5036  ax-pr 5098  ax-un 7184
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-fal 1667  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2592  df-eu 2610  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-ne 2973  df-ral 3095  df-rex 3096  df-reu 3097  df-rab 3099  df-v 3388  df-sbc 3635  df-csb 3730  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-pw 4352  df-sn 4370  df-pr 4372  df-op 4376  df-uni 4630  df-iun 4713  df-br 4845  df-opab 4907  df-mpt 4924  df-id 5221  df-xp 5319  df-rel 5320  df-cnv 5321  df-co 5322  df-dm 5323  df-rn 5324  df-res 5325  df-ima 5326  df-iota 6065  df-fun 6104  df-fn 6105  df-f 6106  df-f1 6107  df-fo 6108  df-f1o 6109  df-fv 6110  df-ov 6882  df-oprab 6883  df-mpt2 6884  df-pm 8099  df-ixp 8150  df-ssc 16783  df-subc 16785
This theorem is referenced by:  issubc2  16809  subcssc  16813
  Copyright terms: Public domain W3C validator