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

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

Proof of Theorem catcxpccl
Dummy variables 𝑓 𝑔 𝑢 𝑣 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 catcxpccl.o . . . . 5 𝑇 = (𝑋 ×c 𝑌)
2 eqid 2820 . . . . 5 (Base‘𝑋) = (Base‘𝑋)
3 eqid 2820 . . . . 5 (Base‘𝑌) = (Base‘𝑌)
4 eqid 2820 . . . . 5 (Hom ‘𝑋) = (Hom ‘𝑋)
5 eqid 2820 . . . . 5 (Hom ‘𝑌) = (Hom ‘𝑌)
6 eqid 2820 . . . . 5 (comp‘𝑋) = (comp‘𝑋)
7 eqid 2820 . . . . 5 (comp‘𝑌) = (comp‘𝑌)
8 catcxpccl.x . . . . 5 (𝜑𝑋𝐵)
9 catcxpccl.y . . . . 5 (𝜑𝑌𝐵)
10 eqidd 2821 . . . . 5 (𝜑 → ((Base‘𝑋) × (Base‘𝑌)) = ((Base‘𝑋) × (Base‘𝑌)))
111, 2, 3xpcbas 17407 . . . . . . 7 ((Base‘𝑋) × (Base‘𝑌)) = (Base‘𝑇)
12 eqid 2820 . . . . . . 7 (Hom ‘𝑇) = (Hom ‘𝑇)
131, 11, 4, 5, 12xpchomfval 17408 . . . . . 6 (Hom ‘𝑇) = (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))))
1413a1i 11 . . . . 5 (𝜑 → (Hom ‘𝑇) = (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣)))))
15 eqidd 2821 . . . . 5 (𝜑 → (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩)) = (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩)))
161, 2, 3, 4, 5, 6, 7, 8, 9, 10, 14, 15xpcval 17406 . . . 4 (𝜑𝑇 = {⟨(Base‘ndx), ((Base‘𝑋) × (Base‘𝑌))⟩, ⟨(Hom ‘ndx), (Hom ‘𝑇)⟩, ⟨(comp‘ndx), (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩))⟩})
17 catcxpccl.u . . . . 5 (𝜑𝑈 ∈ WUni)
18 df-base 16468 . . . . . . 7 Base = Slot 1
19 catcxpccl.1 . . . . . . . 8 (𝜑 → ω ∈ 𝑈)
2017, 19wunndx 16483 . . . . . . 7 (𝜑 → ndx ∈ 𝑈)
2118, 17, 20wunstr 16486 . . . . . 6 (𝜑 → (Base‘ndx) ∈ 𝑈)
22 catcxpccl.c . . . . . . . . . . 11 𝐶 = (CatCat‘𝑈)
23 catcxpccl.b . . . . . . . . . . 11 𝐵 = (Base‘𝐶)
2422, 23, 17catcbas 17336 . . . . . . . . . 10 (𝜑𝐵 = (𝑈 ∩ Cat))
258, 24eleqtrd 2913 . . . . . . . . 9 (𝜑𝑋 ∈ (𝑈 ∩ Cat))
2625elin1d 4153 . . . . . . . 8 (𝜑𝑋𝑈)
2718, 17, 26wunstr 16486 . . . . . . 7 (𝜑 → (Base‘𝑋) ∈ 𝑈)
289, 24eleqtrd 2913 . . . . . . . . 9 (𝜑𝑌 ∈ (𝑈 ∩ Cat))
2928elin1d 4153 . . . . . . . 8 (𝜑𝑌𝑈)
3018, 17, 29wunstr 16486 . . . . . . 7 (𝜑 → (Base‘𝑌) ∈ 𝑈)
3117, 27, 30wunxp 10124 . . . . . 6 (𝜑 → ((Base‘𝑋) × (Base‘𝑌)) ∈ 𝑈)
3217, 21, 31wunop 10122 . . . . 5 (𝜑 → ⟨(Base‘ndx), ((Base‘𝑋) × (Base‘𝑌))⟩ ∈ 𝑈)
33 df-hom 16568 . . . . . . 7 Hom = Slot 14
3433, 17, 20wunstr 16486 . . . . . 6 (𝜑 → (Hom ‘ndx) ∈ 𝑈)
3517, 31, 31wunxp 10124 . . . . . . . 8 (𝜑 → (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) ∈ 𝑈)
3633, 17, 26wunstr 16486 . . . . . . . . . . . 12 (𝜑 → (Hom ‘𝑋) ∈ 𝑈)
3717, 36wunrn 10129 . . . . . . . . . . 11 (𝜑 → ran (Hom ‘𝑋) ∈ 𝑈)
3817, 37wununi 10106 . . . . . . . . . 10 (𝜑 ran (Hom ‘𝑋) ∈ 𝑈)
3933, 17, 29wunstr 16486 . . . . . . . . . . . 12 (𝜑 → (Hom ‘𝑌) ∈ 𝑈)
4017, 39wunrn 10129 . . . . . . . . . . 11 (𝜑 → ran (Hom ‘𝑌) ∈ 𝑈)
4117, 40wununi 10106 . . . . . . . . . 10 (𝜑 ran (Hom ‘𝑌) ∈ 𝑈)
4217, 38, 41wunxp 10124 . . . . . . . . 9 (𝜑 → ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌)) ∈ 𝑈)
4317, 42wunpw 10107 . . . . . . . 8 (𝜑 → 𝒫 ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌)) ∈ 𝑈)
44 ovssunirn 7169 . . . . . . . . . . . . 13 ((1st𝑢)(Hom ‘𝑋)(1st𝑣)) ⊆ ran (Hom ‘𝑋)
45 ovssunirn 7169 . . . . . . . . . . . . 13 ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣)) ⊆ ran (Hom ‘𝑌)
46 xpss12 5546 . . . . . . . . . . . . 13 ((((1st𝑢)(Hom ‘𝑋)(1st𝑣)) ⊆ ran (Hom ‘𝑋) ∧ ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣)) ⊆ ran (Hom ‘𝑌)) → (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))) ⊆ ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌)))
4744, 45, 46mp2an 690 . . . . . . . . . . . 12 (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))) ⊆ ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌))
48 ovex 7166 . . . . . . . . . . . . . 14 ((1st𝑢)(Hom ‘𝑋)(1st𝑣)) ∈ V
49 ovex 7166 . . . . . . . . . . . . . 14 ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣)) ∈ V
5048, 49xpex 7454 . . . . . . . . . . . . 13 (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))) ∈ V
5150elpw 4519 . . . . . . . . . . . 12 ((((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))) ∈ 𝒫 ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌)) ↔ (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))) ⊆ ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌)))
5247, 51mpbir 233 . . . . . . . . . . 11 (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))) ∈ 𝒫 ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌))
5352rgen2w 3138 . . . . . . . . . 10 𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌))∀𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌))(((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))) ∈ 𝒫 ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌))
54 eqid 2820 . . . . . . . . . . 11 (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣)))) = (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))))
5554fmpo 7744 . . . . . . . . . 10 (∀𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌))∀𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌))(((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣))) ∈ 𝒫 ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌)) ↔ (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣)))):(((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))⟶𝒫 ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌)))
5653, 55mpbi 232 . . . . . . . . 9 (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣)))):(((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))⟶𝒫 ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌))
5756a1i 11 . . . . . . . 8 (𝜑 → (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣)))):(((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))⟶𝒫 ( ran (Hom ‘𝑋) × ran (Hom ‘𝑌)))
5817, 35, 43, 57wunf 10127 . . . . . . 7 (𝜑 → (𝑢 ∈ ((Base‘𝑋) × (Base‘𝑌)), 𝑣 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (((1st𝑢)(Hom ‘𝑋)(1st𝑣)) × ((2nd𝑢)(Hom ‘𝑌)(2nd𝑣)))) ∈ 𝑈)
5913, 58eqeltrid 2915 . . . . . 6 (𝜑 → (Hom ‘𝑇) ∈ 𝑈)
6017, 34, 59wunop 10122 . . . . 5 (𝜑 → ⟨(Hom ‘ndx), (Hom ‘𝑇)⟩ ∈ 𝑈)
61 df-cco 16569 . . . . . . 7 comp = Slot 15
6261, 17, 20wunstr 16486 . . . . . 6 (𝜑 → (comp‘ndx) ∈ 𝑈)
6317, 35, 31wunxp 10124 . . . . . . 7 (𝜑 → ((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌))) ∈ 𝑈)
6461, 17, 26wunstr 16486 . . . . . . . . . . . . . 14 (𝜑 → (comp‘𝑋) ∈ 𝑈)
6517, 64wunrn 10129 . . . . . . . . . . . . 13 (𝜑 → ran (comp‘𝑋) ∈ 𝑈)
6617, 65wununi 10106 . . . . . . . . . . . 12 (𝜑 ran (comp‘𝑋) ∈ 𝑈)
6717, 66wunrn 10129 . . . . . . . . . . 11 (𝜑 → ran ran (comp‘𝑋) ∈ 𝑈)
6817, 67wununi 10106 . . . . . . . . . 10 (𝜑 ran ran (comp‘𝑋) ∈ 𝑈)
6917, 68wunpw 10107 . . . . . . . . 9 (𝜑 → 𝒫 ran ran (comp‘𝑋) ∈ 𝑈)
7061, 17, 29wunstr 16486 . . . . . . . . . . . . . 14 (𝜑 → (comp‘𝑌) ∈ 𝑈)
7117, 70wunrn 10129 . . . . . . . . . . . . 13 (𝜑 → ran (comp‘𝑌) ∈ 𝑈)
7217, 71wununi 10106 . . . . . . . . . . . 12 (𝜑 ran (comp‘𝑌) ∈ 𝑈)
7317, 72wunrn 10129 . . . . . . . . . . 11 (𝜑 → ran ran (comp‘𝑌) ∈ 𝑈)
7417, 73wununi 10106 . . . . . . . . . 10 (𝜑 ran ran (comp‘𝑌) ∈ 𝑈)
7517, 74wunpw 10107 . . . . . . . . 9 (𝜑 → 𝒫 ran ran (comp‘𝑌) ∈ 𝑈)
7617, 69, 75wunxp 10124 . . . . . . . 8 (𝜑 → (𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ∈ 𝑈)
7717, 59wunrn 10129 . . . . . . . . . 10 (𝜑 → ran (Hom ‘𝑇) ∈ 𝑈)
7817, 77wununi 10106 . . . . . . . . 9 (𝜑 ran (Hom ‘𝑇) ∈ 𝑈)
7917, 78, 78wunxp 10124 . . . . . . . 8 (𝜑 → ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇)) ∈ 𝑈)
8017, 76, 79wunpm 10125 . . . . . . 7 (𝜑 → ((𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ↑pm ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇))) ∈ 𝑈)
81 fvex 6659 . . . . . . . . . . . . . . . . 17 (comp‘𝑋) ∈ V
8281rnex 7595 . . . . . . . . . . . . . . . 16 ran (comp‘𝑋) ∈ V
8382uniex 7445 . . . . . . . . . . . . . . 15 ran (comp‘𝑋) ∈ V
8483rnex 7595 . . . . . . . . . . . . . 14 ran ran (comp‘𝑋) ∈ V
8584uniex 7445 . . . . . . . . . . . . 13 ran ran (comp‘𝑋) ∈ V
8685pwex 5257 . . . . . . . . . . . 12 𝒫 ran ran (comp‘𝑋) ∈ V
87 fvex 6659 . . . . . . . . . . . . . . . . 17 (comp‘𝑌) ∈ V
8887rnex 7595 . . . . . . . . . . . . . . . 16 ran (comp‘𝑌) ∈ V
8988uniex 7445 . . . . . . . . . . . . . . 15 ran (comp‘𝑌) ∈ V
9089rnex 7595 . . . . . . . . . . . . . 14 ran ran (comp‘𝑌) ∈ V
9190uniex 7445 . . . . . . . . . . . . 13 ran ran (comp‘𝑌) ∈ V
9291pwex 5257 . . . . . . . . . . . 12 𝒫 ran ran (comp‘𝑌) ∈ V
9386, 92xpex 7454 . . . . . . . . . . 11 (𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ∈ V
94 fvex 6659 . . . . . . . . . . . . . 14 (Hom ‘𝑇) ∈ V
9594rnex 7595 . . . . . . . . . . . . 13 ran (Hom ‘𝑇) ∈ V
9695uniex 7445 . . . . . . . . . . . 12 ran (Hom ‘𝑇) ∈ V
9796, 96xpex 7454 . . . . . . . . . . 11 ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇)) ∈ V
98 ovssunirn 7169 . . . . . . . . . . . . . . . 16 ((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)) ⊆ ran (⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))
99 ovssunirn 7169 . . . . . . . . . . . . . . . . 17 (⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦)) ⊆ ran (comp‘𝑋)
100 rnss 5785 . . . . . . . . . . . . . . . . 17 ((⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦)) ⊆ ran (comp‘𝑋) → ran (⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦)) ⊆ ran ran (comp‘𝑋))
101 uniss 4822 . . . . . . . . . . . . . . . . 17 (ran (⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦)) ⊆ ran ran (comp‘𝑋) → ran (⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦)) ⊆ ran ran (comp‘𝑋))
10299, 100, 101mp2b 10 . . . . . . . . . . . . . . . 16 ran (⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦)) ⊆ ran ran (comp‘𝑋)
10398, 102sstri 3955 . . . . . . . . . . . . . . 15 ((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)) ⊆ ran ran (comp‘𝑋)
104 ovex 7166 . . . . . . . . . . . . . . . 16 ((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)) ∈ V
105104elpw 4519 . . . . . . . . . . . . . . 15 (((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)) ∈ 𝒫 ran ran (comp‘𝑋) ↔ ((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)) ⊆ ran ran (comp‘𝑋))
106103, 105mpbir 233 . . . . . . . . . . . . . 14 ((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)) ∈ 𝒫 ran ran (comp‘𝑋)
107 ovssunirn 7169 . . . . . . . . . . . . . . . 16 ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓)) ⊆ ran (⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))
108 ovssunirn 7169 . . . . . . . . . . . . . . . . 17 (⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦)) ⊆ ran (comp‘𝑌)
109 rnss 5785 . . . . . . . . . . . . . . . . 17 ((⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦)) ⊆ ran (comp‘𝑌) → ran (⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦)) ⊆ ran ran (comp‘𝑌))
110 uniss 4822 . . . . . . . . . . . . . . . . 17 (ran (⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦)) ⊆ ran ran (comp‘𝑌) → ran (⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦)) ⊆ ran ran (comp‘𝑌))
111108, 109, 110mp2b 10 . . . . . . . . . . . . . . . 16 ran (⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦)) ⊆ ran ran (comp‘𝑌)
112107, 111sstri 3955 . . . . . . . . . . . . . . 15 ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓)) ⊆ ran ran (comp‘𝑌)
113 ovex 7166 . . . . . . . . . . . . . . . 16 ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓)) ∈ V
114113elpw 4519 . . . . . . . . . . . . . . 15 (((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓)) ∈ 𝒫 ran ran (comp‘𝑌) ↔ ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓)) ⊆ ran ran (comp‘𝑌))
115112, 114mpbir 233 . . . . . . . . . . . . . 14 ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓)) ∈ 𝒫 ran ran (comp‘𝑌)
116 opelxpi 5568 . . . . . . . . . . . . . 14 ((((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)) ∈ 𝒫 ran ran (comp‘𝑋) ∧ ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓)) ∈ 𝒫 ran ran (comp‘𝑌)) → ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩ ∈ (𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)))
117106, 115, 116mp2an 690 . . . . . . . . . . . . 13 ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩ ∈ (𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌))
118117rgen2w 3138 . . . . . . . . . . . 12 𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦)∀𝑓 ∈ ((Hom ‘𝑇)‘𝑥)⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩ ∈ (𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌))
119 eqid 2820 . . . . . . . . . . . . 13 (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩) = (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩)
120119fmpo 7744 . . . . . . . . . . . 12 (∀𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦)∀𝑓 ∈ ((Hom ‘𝑇)‘𝑥)⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩ ∈ (𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ↔ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩):(((2nd𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥))⟶(𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)))
121118, 120mpbi 232 . . . . . . . . . . 11 (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩):(((2nd𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥))⟶(𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌))
122 ovssunirn 7169 . . . . . . . . . . . 12 ((2nd𝑥)(Hom ‘𝑇)𝑦) ⊆ ran (Hom ‘𝑇)
123 fvssunirn 6675 . . . . . . . . . . . 12 ((Hom ‘𝑇)‘𝑥) ⊆ ran (Hom ‘𝑇)
124 xpss12 5546 . . . . . . . . . . . 12 ((((2nd𝑥)(Hom ‘𝑇)𝑦) ⊆ ran (Hom ‘𝑇) ∧ ((Hom ‘𝑇)‘𝑥) ⊆ ran (Hom ‘𝑇)) → (((2nd𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥)) ⊆ ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇)))
125122, 123, 124mp2an 690 . . . . . . . . . . 11 (((2nd𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥)) ⊆ ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇))
126 elpm2r 8402 . . . . . . . . . . 11 ((((𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ∈ V ∧ ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇)) ∈ V) ∧ ((𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩):(((2nd𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥))⟶(𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ∧ (((2nd𝑥)(Hom ‘𝑇)𝑦) × ((Hom ‘𝑇)‘𝑥)) ⊆ ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇)))) → (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩) ∈ ((𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ↑pm ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇))))
12793, 97, 121, 125, 126mp4an 691 . . . . . . . . . 10 (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩) ∈ ((𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ↑pm ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇)))
128127rgen2w 3138 . . . . . . . . 9 𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))∀𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌))(𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩) ∈ ((𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ↑pm ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇)))
129 eqid 2820 . . . . . . . . . 10 (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩)) = (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩))
130129fmpo 7744 . . . . . . . . 9 (∀𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌)))∀𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌))(𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩) ∈ ((𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ↑pm ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇))) ↔ (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩)):((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌)))⟶((𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ↑pm ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇))))
131128, 130mpbi 232 . . . . . . . 8 (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩)):((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌)))⟶((𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ↑pm ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇)))
132131a1i 11 . . . . . . 7 (𝜑 → (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩)):((((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))) × ((Base‘𝑋) × (Base‘𝑌)))⟶((𝒫 ran ran (comp‘𝑋) × 𝒫 ran ran (comp‘𝑌)) ↑pm ( ran (Hom ‘𝑇) × ran (Hom ‘𝑇))))
13317, 63, 80, 132wunf 10127 . . . . . 6 (𝜑 → (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩)) ∈ 𝑈)
13417, 62, 133wunop 10122 . . . . 5 (𝜑 → ⟨(comp‘ndx), (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩))⟩ ∈ 𝑈)
13517, 32, 60, 134wuntp 10111 . . . 4 (𝜑 → {⟨(Base‘ndx), ((Base‘𝑋) × (Base‘𝑌))⟩, ⟨(Hom ‘ndx), (Hom ‘𝑇)⟩, ⟨(comp‘ndx), (𝑥 ∈ (((Base‘𝑋) × (Base‘𝑌)) × ((Base‘𝑋) × (Base‘𝑌))), 𝑦 ∈ ((Base‘𝑋) × (Base‘𝑌)) ↦ (𝑔 ∈ ((2nd𝑥)(Hom ‘𝑇)𝑦), 𝑓 ∈ ((Hom ‘𝑇)‘𝑥) ↦ ⟨((1st𝑔)(⟨(1st ‘(1st𝑥)), (1st ‘(2nd𝑥))⟩(comp‘𝑋)(1st𝑦))(1st𝑓)), ((2nd𝑔)(⟨(2nd ‘(1st𝑥)), (2nd ‘(2nd𝑥))⟩(comp‘𝑌)(2nd𝑦))(2nd𝑓))⟩))⟩} ∈ 𝑈)
13616, 135eqeltrd 2911 . . 3 (𝜑𝑇𝑈)
13725elin2d 4154 . . . 4 (𝜑𝑋 ∈ Cat)
13828elin2d 4154 . . . 4 (𝜑𝑌 ∈ Cat)
1391, 137, 138xpccat 17419 . . 3 (𝜑𝑇 ∈ Cat)
140136, 139elind 4149 . 2 (𝜑𝑇 ∈ (𝑈 ∩ Cat))
141140, 24eleqtrrd 2914 1 (𝜑𝑇𝐵)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1537   ∈ wcel 2114  ∀wral 3125  Vcvv 3473   ∩ cin 3912   ⊆ wss 3913  𝒫 cpw 4515  {ctp 4547  ⟨cop 4549  ∪ cuni 4814   × cxp 5529  ran crn 5532  ⟶wf 6327  ‘cfv 6331  (class class class)co 7133   ∈ cmpo 7135  ωcom 7558  1st c1st 7665  2nd c2nd 7666   ↑pm cpm 8385  WUnicwun 10100  1c1 10516  4c4 11673  5c5 11674  ;cdc 12077  ndxcnx 16459  Basecbs 16462  Hom chom 16555  compcco 16556  Catccat 16914  CatCatccatc 17333   ×c cxpc 17397 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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2792  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5242  ax-pr 5306  ax-un 7439  ax-inf2 9082  ax-cnex 10571  ax-resscn 10572  ax-1cn 10573  ax-icn 10574  ax-addcl 10575  ax-addrcl 10576  ax-mulcl 10577  ax-mulrcl 10578  ax-mulcom 10579  ax-addass 10580  ax-mulass 10581  ax-distr 10582  ax-i2m1 10583  ax-1ne0 10584  ax-1rid 10585  ax-rnegex 10586  ax-rrecex 10587  ax-cnre 10588  ax-pre-lttri 10589  ax-pre-lttrn 10590  ax-pre-ltadd 10591  ax-pre-mulgt0 10592 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-fal 1550  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2799  df-cleq 2813  df-clel 2891  df-nfc 2959  df-ne 3007  df-nel 3111  df-ral 3130  df-rex 3131  df-reu 3132  df-rmo 3133  df-rab 3134  df-v 3475  df-sbc 3753  df-csb 3861  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3932  df-nul 4270  df-if 4444  df-pw 4517  df-sn 4544  df-pr 4546  df-tp 4548  df-op 4550  df-uni 4815  df-int 4853  df-iun 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5436  df-eprel 5441  df-po 5450  df-so 5451  df-fr 5490  df-we 5492  df-xp 5537  df-rel 5538  df-cnv 5539  df-co 5540  df-dm 5541  df-rn 5542  df-res 5543  df-ima 5544  df-pred 6124  df-ord 6170  df-on 6171  df-lim 6172  df-suc 6173  df-iota 6290  df-fun 6333  df-fn 6334  df-f 6335  df-f1 6336  df-fo 6337  df-f1o 6338  df-fv 6339  df-riota 7091  df-ov 7136  df-oprab 7137  df-mpo 7138  df-om 7559  df-1st 7667  df-2nd 7668  df-wrecs 7925  df-recs 7986  df-rdg 8024  df-1o 8080  df-oadd 8084  df-omul 8085  df-er 8267  df-ec 8269  df-qs 8273  df-map 8386  df-pm 8387  df-en 8488  df-dom 8489  df-sdom 8490  df-fin 8491  df-wun 10102  df-ni 10272  df-pli 10273  df-mi 10274  df-lti 10275  df-plpq 10308  df-mpq 10309  df-ltpq 10310  df-enq 10311  df-nq 10312  df-erq 10313  df-plq 10314  df-mq 10315  df-1nq 10316  df-rq 10317  df-ltnq 10318  df-np 10381  df-plp 10383  df-ltp 10385  df-enr 10455  df-nr 10456  df-c 10521  df-pnf 10655  df-mnf 10656  df-xr 10657  df-ltxr 10658  df-le 10659  df-sub 10850  df-neg 10851  df-nn 11617  df-2 11679  df-3 11680  df-4 11681  df-5 11682  df-6 11683  df-7 11684  df-8 11685  df-9 11686  df-n0 11877  df-z 11961  df-dec 12078  df-uz 12223  df-fz 12877  df-struct 16464  df-ndx 16465  df-slot 16466  df-base 16468  df-hom 16568  df-cco 16569  df-cat 16918  df-cid 16919  df-catc 17334  df-xpc 17401 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator