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

Theorem catcfuccl 17435
 Description: The category of categories for a weak universe is closed under the functor category operation. (Contributed by Mario Carneiro, 12-Jan-2017.)
Hypotheses
Ref Expression
catcfuccl.c 𝐶 = (CatCat‘𝑈)
catcfuccl.b 𝐵 = (Base‘𝐶)
catcfuccl.o 𝑄 = (𝑋 FuncCat 𝑌)
catcfuccl.u (𝜑𝑈 ∈ WUni)
catcfuccl.1 (𝜑 → ω ∈ 𝑈)
catcfuccl.x (𝜑𝑋𝐵)
catcfuccl.y (𝜑𝑌𝐵)
Assertion
Ref Expression
catcfuccl (𝜑𝑄𝐵)

Proof of Theorem catcfuccl
Dummy variables 𝑎 𝑏 𝑓 𝑔 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcfuccl.o . . . . 5 𝑄 = (𝑋 FuncCat 𝑌)
2 eqid 2758 . . . . 5 (𝑋 Func 𝑌) = (𝑋 Func 𝑌)
3 eqid 2758 . . . . 5 (𝑋 Nat 𝑌) = (𝑋 Nat 𝑌)
4 eqid 2758 . . . . 5 (Base‘𝑋) = (Base‘𝑋)
5 eqid 2758 . . . . 5 (comp‘𝑌) = (comp‘𝑌)
6 catcfuccl.x . . . . . . 7 (𝜑𝑋𝐵)
7 catcfuccl.c . . . . . . . 8 𝐶 = (CatCat‘𝑈)
8 catcfuccl.b . . . . . . . 8 𝐵 = (Base‘𝐶)
9 catcfuccl.u . . . . . . . 8 (𝜑𝑈 ∈ WUni)
107, 8, 9catcbas 17423 . . . . . . 7 (𝜑𝐵 = (𝑈 ∩ Cat))
116, 10eleqtrd 2854 . . . . . 6 (𝜑𝑋 ∈ (𝑈 ∩ Cat))
1211elin2d 4104 . . . . 5 (𝜑𝑋 ∈ Cat)
13 catcfuccl.y . . . . . . 7 (𝜑𝑌𝐵)
1413, 10eleqtrd 2854 . . . . . 6 (𝜑𝑌 ∈ (𝑈 ∩ Cat))
1514elin2d 4104 . . . . 5 (𝜑𝑌 ∈ Cat)
16 eqidd 2759 . . . . 5 (𝜑 → (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))))) = (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))))))
171, 2, 3, 4, 5, 12, 15, 16fucval 17287 . . . 4 (𝜑𝑄 = {⟨(Base‘ndx), (𝑋 Func 𝑌)⟩, ⟨(Hom ‘ndx), (𝑋 Nat 𝑌)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))))⟩})
18 df-base 16547 . . . . . . 7 Base = Slot 1
19 catcfuccl.1 . . . . . . . 8 (𝜑 → ω ∈ 𝑈)
209, 19wunndx 16562 . . . . . . 7 (𝜑 → ndx ∈ 𝑈)
2118, 9, 20wunstr 16565 . . . . . 6 (𝜑 → (Base‘ndx) ∈ 𝑈)
2211elin1d 4103 . . . . . . 7 (𝜑𝑋𝑈)
2314elin1d 4103 . . . . . . 7 (𝜑𝑌𝑈)
249, 22, 23wunfunc 17228 . . . . . 6 (𝜑 → (𝑋 Func 𝑌) ∈ 𝑈)
259, 21, 24wunop 10182 . . . . 5 (𝜑 → ⟨(Base‘ndx), (𝑋 Func 𝑌)⟩ ∈ 𝑈)
26 df-hom 16647 . . . . . . 7 Hom = Slot 14
2726, 9, 20wunstr 16565 . . . . . 6 (𝜑 → (Hom ‘ndx) ∈ 𝑈)
289, 22, 23wunnat 17285 . . . . . 6 (𝜑 → (𝑋 Nat 𝑌) ∈ 𝑈)
299, 27, 28wunop 10182 . . . . 5 (𝜑 → ⟨(Hom ‘ndx), (𝑋 Nat 𝑌)⟩ ∈ 𝑈)
30 df-cco 16648 . . . . . . 7 comp = Slot 15
3130, 9, 20wunstr 16565 . . . . . 6 (𝜑 → (comp‘ndx) ∈ 𝑈)
329, 24, 24wunxp 10184 . . . . . . . 8 (𝜑 → ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) ∈ 𝑈)
339, 32, 24wunxp 10184 . . . . . . 7 (𝜑 → (((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌)) ∈ 𝑈)
3430, 9, 23wunstr 16565 . . . . . . . . . . . . . 14 (𝜑 → (comp‘𝑌) ∈ 𝑈)
359, 34wunrn 10189 . . . . . . . . . . . . 13 (𝜑 → ran (comp‘𝑌) ∈ 𝑈)
369, 35wununi 10166 . . . . . . . . . . . 12 (𝜑 ran (comp‘𝑌) ∈ 𝑈)
379, 36wunrn 10189 . . . . . . . . . . 11 (𝜑 → ran ran (comp‘𝑌) ∈ 𝑈)
389, 37wununi 10166 . . . . . . . . . 10 (𝜑 ran ran (comp‘𝑌) ∈ 𝑈)
399, 38wunpw 10167 . . . . . . . . 9 (𝜑 → 𝒫 ran ran (comp‘𝑌) ∈ 𝑈)
4018, 9, 22wunstr 16565 . . . . . . . . 9 (𝜑 → (Base‘𝑋) ∈ 𝑈)
419, 39, 40wunmap 10186 . . . . . . . 8 (𝜑 → (𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ∈ 𝑈)
429, 28wunrn 10189 . . . . . . . . . 10 (𝜑 → ran (𝑋 Nat 𝑌) ∈ 𝑈)
439, 42wununi 10166 . . . . . . . . 9 (𝜑 ran (𝑋 Nat 𝑌) ∈ 𝑈)
449, 43, 43wunxp 10184 . . . . . . . 8 (𝜑 → ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)) ∈ 𝑈)
459, 41, 44wunpm 10185 . . . . . . 7 (𝜑 → ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))) ∈ 𝑈)
46 fvex 6671 . . . . . . . . . . 11 (1st𝑣) ∈ V
47 fvex 6671 . . . . . . . . . . . . . 14 (2nd𝑣) ∈ V
48 ovex 7183 . . . . . . . . . . . . . . . . 17 (𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ∈ V
49 ovex 7183 . . . . . . . . . . . . . . . . . . . 20 (𝑋 Nat 𝑌) ∈ V
5049rnex 7622 . . . . . . . . . . . . . . . . . . 19 ran (𝑋 Nat 𝑌) ∈ V
5150uniex 7465 . . . . . . . . . . . . . . . . . 18 ran (𝑋 Nat 𝑌) ∈ V
5251, 51xpex 7474 . . . . . . . . . . . . . . . . 17 ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)) ∈ V
53 eqid 2758 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))) = (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))
54 ovssunirn 7186 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)) ⊆ ran (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))
55 ovssunirn 7186 . . . . . . . . . . . . . . . . . . . . . . . . 25 (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥)) ⊆ ran (comp‘𝑌)
56 rnss 5780 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥)) ⊆ ran (comp‘𝑌) → ran (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥)) ⊆ ran ran (comp‘𝑌))
57 uniss 4806 . . . . . . . . . . . . . . . . . . . . . . . . 25 (ran (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥)) ⊆ ran ran (comp‘𝑌) → ran (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥)) ⊆ ran ran (comp‘𝑌))
5855, 56, 57mp2b 10 . . . . . . . . . . . . . . . . . . . . . . . 24 ran (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥)) ⊆ ran ran (comp‘𝑌)
5954, 58sstri 3901 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)) ⊆ ran ran (comp‘𝑌)
60 ovex 7183 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)) ∈ V
6160elpw 4498 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)) ∈ 𝒫 ran ran (comp‘𝑌) ↔ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)) ⊆ ran ran (comp‘𝑌))
6259, 61mpbir 234 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)) ∈ 𝒫 ran ran (comp‘𝑌)
6362a1i 11 . . . . . . . . . . . . . . . . . . . . 21 (𝑥 ∈ (Base‘𝑋) → ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)) ∈ 𝒫 ran ran (comp‘𝑌))
6453, 63fmpti 6867 . . . . . . . . . . . . . . . . . . . 20 (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))):(Base‘𝑋)⟶𝒫 ran ran (comp‘𝑌)
65 fvex 6671 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (comp‘𝑌) ∈ V
6665rnex 7622 . . . . . . . . . . . . . . . . . . . . . . . . 25 ran (comp‘𝑌) ∈ V
6766uniex 7465 . . . . . . . . . . . . . . . . . . . . . . . 24 ran (comp‘𝑌) ∈ V
6867rnex 7622 . . . . . . . . . . . . . . . . . . . . . . 23 ran ran (comp‘𝑌) ∈ V
6968uniex 7465 . . . . . . . . . . . . . . . . . . . . . 22 ran ran (comp‘𝑌) ∈ V
7069pwex 5249 . . . . . . . . . . . . . . . . . . . . 21 𝒫 ran ran (comp‘𝑌) ∈ V
71 fvex 6671 . . . . . . . . . . . . . . . . . . . . 21 (Base‘𝑋) ∈ V
7270, 71elmap 8453 . . . . . . . . . . . . . . . . . . . 20 ((𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))) ∈ (𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↔ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))):(Base‘𝑋)⟶𝒫 ran ran (comp‘𝑌))
7364, 72mpbir 234 . . . . . . . . . . . . . . . . . . 19 (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))) ∈ (𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋))
7473rgen2w 3083 . . . . . . . . . . . . . . . . . 18 𝑏 ∈ (𝑔(𝑋 Nat 𝑌))∀𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔)(𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))) ∈ (𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋))
75 eqid 2758 . . . . . . . . . . . . . . . . . . 19 (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) = (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))))
7675fmpo 7770 . . . . . . . . . . . . . . . . . 18 (∀𝑏 ∈ (𝑔(𝑋 Nat 𝑌))∀𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔)(𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))) ∈ (𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↔ (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))):((𝑔(𝑋 Nat 𝑌)) × (𝑓(𝑋 Nat 𝑌)𝑔))⟶(𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)))
7774, 76mpbi 233 . . . . . . . . . . . . . . . . 17 (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))):((𝑔(𝑋 Nat 𝑌)) × (𝑓(𝑋 Nat 𝑌)𝑔))⟶(𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋))
78 ovssunirn 7186 . . . . . . . . . . . . . . . . . 18 (𝑔(𝑋 Nat 𝑌)) ⊆ ran (𝑋 Nat 𝑌)
79 ovssunirn 7186 . . . . . . . . . . . . . . . . . 18 (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ran (𝑋 Nat 𝑌)
80 xpss12 5539 . . . . . . . . . . . . . . . . . 18 (((𝑔(𝑋 Nat 𝑌)) ⊆ ran (𝑋 Nat 𝑌) ∧ (𝑓(𝑋 Nat 𝑌)𝑔) ⊆ ran (𝑋 Nat 𝑌)) → ((𝑔(𝑋 Nat 𝑌)) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)))
8178, 79, 80mp2an 691 . . . . . . . . . . . . . . . . 17 ((𝑔(𝑋 Nat 𝑌)) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))
82 elpm2r 8434 . . . . . . . . . . . . . . . . 17 ((((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ∈ V ∧ ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)) ∈ V) ∧ ((𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))):((𝑔(𝑋 Nat 𝑌)) × (𝑓(𝑋 Nat 𝑌)𝑔))⟶(𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ∧ ((𝑔(𝑋 Nat 𝑌)) × (𝑓(𝑋 Nat 𝑌)𝑔)) ⊆ ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)))) → (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))))
8348, 52, 77, 81, 82mp4an 692 . . . . . . . . . . . . . . . 16 (𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)))
8483sbcth 3711 . . . . . . . . . . . . . . 15 ((2nd𝑣) ∈ V → [(2nd𝑣) / 𝑔](𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))))
85 sbcel1g 4310 . . . . . . . . . . . . . . 15 ((2nd𝑣) ∈ V → ([(2nd𝑣) / 𝑔](𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))) ↔ (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)))))
8684, 85mpbid 235 . . . . . . . . . . . . . 14 ((2nd𝑣) ∈ V → (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))))
8747, 86ax-mp 5 . . . . . . . . . . . . 13 (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)))
8887sbcth 3711 . . . . . . . . . . . 12 ((1st𝑣) ∈ V → [(1st𝑣) / 𝑓](2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))))
89 sbcel1g 4310 . . . . . . . . . . . 12 ((1st𝑣) ∈ V → ([(1st𝑣) / 𝑓](2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))) ↔ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)))))
9088, 89mpbid 235 . . . . . . . . . . 11 ((1st𝑣) ∈ V → (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))))
9146, 90ax-mp 5 . . . . . . . . . 10 (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)))
9291rgen2w 3083 . . . . . . . . 9 𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌))∀ ∈ (𝑋 Func 𝑌)(1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)))
93 eqid 2758 . . . . . . . . . 10 (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))))) = (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))))
9493fmpo 7770 . . . . . . . . 9 (∀𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌))∀ ∈ (𝑋 Func 𝑌)(1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))) ∈ ((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))) ↔ (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))))):(((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌))⟶((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))))
9592, 94mpbi 233 . . . . . . . 8 (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))))):(((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌))⟶((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌)))
9695a1i 11 . . . . . . 7 (𝜑 → (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))))):(((𝑋 Func 𝑌) × (𝑋 Func 𝑌)) × (𝑋 Func 𝑌))⟶((𝒫 ran ran (comp‘𝑌) ↑m (Base‘𝑋)) ↑pm ( ran (𝑋 Nat 𝑌) × ran (𝑋 Nat 𝑌))))
979, 33, 45, 96wunf 10187 . . . . . 6 (𝜑 → (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥))))) ∈ 𝑈)
989, 31, 97wunop 10182 . . . . 5 (𝜑 → ⟨(comp‘ndx), (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))))⟩ ∈ 𝑈)
999, 25, 29, 98wuntp 10171 . . . 4 (𝜑 → {⟨(Base‘ndx), (𝑋 Func 𝑌)⟩, ⟨(Hom ‘ndx), (𝑋 Nat 𝑌)⟩, ⟨(comp‘ndx), (𝑣 ∈ ((𝑋 Func 𝑌) × (𝑋 Func 𝑌)), ∈ (𝑋 Func 𝑌) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔(𝑋 Nat 𝑌)), 𝑎 ∈ (𝑓(𝑋 Nat 𝑌)𝑔) ↦ (𝑥 ∈ (Base‘𝑋) ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩(comp‘𝑌)((1st)‘𝑥))(𝑎𝑥)))))⟩} ∈ 𝑈)
10017, 99eqeltrd 2852 . . 3 (𝜑𝑄𝑈)
1011, 12, 15fuccat 17299 . . 3 (𝜑𝑄 ∈ Cat)
102100, 101elind 4099 . 2 (𝜑𝑄 ∈ (𝑈 ∩ Cat))
103102, 10eleqtrrd 2855 1 (𝜑𝑄𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ∈ wcel 2111  ∀wral 3070  Vcvv 3409  [wsbc 3696  ⦋csb 3805   ∩ cin 3857   ⊆ wss 3858  𝒫 cpw 4494  {ctp 4526  ⟨cop 4528  ∪ cuni 4798   ↦ cmpt 5112   × cxp 5522  ran crn 5525  ⟶wf 6331  ‘cfv 6335  (class class class)co 7150   ∈ cmpo 7152  ωcom 7579  1st c1st 7691  2nd c2nd 7692   ↑m cmap 8416   ↑pm cpm 8417  WUnicwun 10160  1c1 10576  4c4 11731  5c5 11732  ;cdc 12137  ndxcnx 16538  Basecbs 16541  Hom chom 16634  compcco 16635  Catccat 16993   Func cfunc 17183   Nat cnat 17270   FuncCat cfuc 17271  CatCatccatc 17420 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-inf2 9137  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-int 4839  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-om 7580  df-1st 7693  df-2nd 7694  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-oadd 8116  df-omul 8117  df-er 8299  df-ec 8301  df-qs 8305  df-map 8418  df-pm 8419  df-ixp 8480  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-wun 10162  df-ni 10332  df-pli 10333  df-mi 10334  df-lti 10335  df-plpq 10368  df-mpq 10369  df-ltpq 10370  df-enq 10371  df-nq 10372  df-erq 10373  df-plq 10374  df-mq 10375  df-1nq 10376  df-rq 10377  df-ltnq 10378  df-np 10441  df-plp 10443  df-ltp 10445  df-enr 10515  df-nr 10516  df-c 10581  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-nn 11675  df-2 11737  df-3 11738  df-4 11739  df-5 11740  df-6 11741  df-7 11742  df-8 11743  df-9 11744  df-n0 11935  df-z 12021  df-dec 12138  df-uz 12283  df-fz 12940  df-struct 16543  df-ndx 16544  df-slot 16545  df-base 16547  df-hom 16647  df-cco 16648  df-cat 16997  df-cid 16998  df-func 17187  df-nat 17272  df-fuc 17273  df-catc 17421 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator