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

Theorem fucval 17909
Description: Value of the functor category. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
fucval.q 𝑄 = (𝐢 FuncCat 𝐷)
fucval.b 𝐡 = (𝐢 Func 𝐷)
fucval.n 𝑁 = (𝐢 Nat 𝐷)
fucval.a 𝐴 = (Baseβ€˜πΆ)
fucval.o Β· = (compβ€˜π·)
fucval.c (πœ‘ β†’ 𝐢 ∈ Cat)
fucval.d (πœ‘ β†’ 𝐷 ∈ Cat)
fucval.x (πœ‘ β†’ βˆ™ = (𝑣 ∈ (𝐡 Γ— 𝐡), β„Ž ∈ 𝐡 ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (π‘”π‘β„Ž), π‘Ž ∈ (𝑓𝑁𝑔) ↦ (π‘₯ ∈ 𝐴 ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))))
Assertion
Ref Expression
fucval (πœ‘ β†’ 𝑄 = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), π‘βŸ©, ⟨(compβ€˜ndx), βˆ™ ⟩})
Distinct variable groups:   𝑣,β„Ž,𝐡   π‘Ž,𝑏,𝑓,𝑔,β„Ž,𝑣,π‘₯,πœ‘   𝐢,π‘Ž,𝑏,𝑓,𝑔,β„Ž,𝑣,π‘₯   𝐷,π‘Ž,𝑏,𝑓,𝑔,β„Ž,𝑣,π‘₯
Allowed substitution hints:   𝐴(π‘₯,𝑣,𝑓,𝑔,β„Ž,π‘Ž,𝑏)   𝐡(π‘₯,𝑓,𝑔,π‘Ž,𝑏)   𝑄(π‘₯,𝑣,𝑓,𝑔,β„Ž,π‘Ž,𝑏)   βˆ™ (π‘₯,𝑣,𝑓,𝑔,β„Ž,π‘Ž,𝑏)   Β· (π‘₯,𝑣,𝑓,𝑔,β„Ž,π‘Ž,𝑏)   𝑁(π‘₯,𝑣,𝑓,𝑔,β„Ž,π‘Ž,𝑏)

Proof of Theorem fucval
Dummy variables 𝑑 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fucval.q . 2 𝑄 = (𝐢 FuncCat 𝐷)
2 df-fuc 17894 . . . 4 FuncCat = (𝑑 ∈ Cat, 𝑒 ∈ Cat ↦ {⟨(Baseβ€˜ndx), (𝑑 Func 𝑒)⟩, ⟨(Hom β€˜ndx), (𝑑 Nat 𝑒)⟩, ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒)), β„Ž ∈ (𝑑 Func 𝑒) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩})
32a1i 11 . . 3 (πœ‘ β†’ FuncCat = (𝑑 ∈ Cat, 𝑒 ∈ Cat ↦ {⟨(Baseβ€˜ndx), (𝑑 Func 𝑒)⟩, ⟨(Hom β€˜ndx), (𝑑 Nat 𝑒)⟩, ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒)), β„Ž ∈ (𝑑 Func 𝑒) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩}))
4 simprl 769 . . . . . . 7 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ 𝑑 = 𝐢)
5 simprr 771 . . . . . . 7 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ 𝑒 = 𝐷)
64, 5oveq12d 7426 . . . . . 6 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (𝑑 Func 𝑒) = (𝐢 Func 𝐷))
7 fucval.b . . . . . 6 𝐡 = (𝐢 Func 𝐷)
86, 7eqtr4di 2790 . . . . 5 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (𝑑 Func 𝑒) = 𝐡)
98opeq2d 4880 . . . 4 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ ⟨(Baseβ€˜ndx), (𝑑 Func 𝑒)⟩ = ⟨(Baseβ€˜ndx), 𝐡⟩)
104, 5oveq12d 7426 . . . . . 6 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (𝑑 Nat 𝑒) = (𝐢 Nat 𝐷))
11 fucval.n . . . . . 6 𝑁 = (𝐢 Nat 𝐷)
1210, 11eqtr4di 2790 . . . . 5 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (𝑑 Nat 𝑒) = 𝑁)
1312opeq2d 4880 . . . 4 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ ⟨(Hom β€˜ndx), (𝑑 Nat 𝑒)⟩ = ⟨(Hom β€˜ndx), π‘βŸ©)
148sqxpeqd 5708 . . . . . . 7 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒)) = (𝐡 Γ— 𝐡))
1512oveqd 7425 . . . . . . . . . 10 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (𝑔(𝑑 Nat 𝑒)β„Ž) = (π‘”π‘β„Ž))
1612oveqd 7425 . . . . . . . . . 10 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (𝑓(𝑑 Nat 𝑒)𝑔) = (𝑓𝑁𝑔))
174fveq2d 6895 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (Baseβ€˜π‘‘) = (Baseβ€˜πΆ))
18 fucval.a . . . . . . . . . . . 12 𝐴 = (Baseβ€˜πΆ)
1917, 18eqtr4di 2790 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (Baseβ€˜π‘‘) = 𝐴)
205fveq2d 6895 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (compβ€˜π‘’) = (compβ€˜π·))
21 fucval.o . . . . . . . . . . . . . 14 Β· = (compβ€˜π·)
2220, 21eqtr4di 2790 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (compβ€˜π‘’) = Β· )
2322oveqd 7425 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯)) = (⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯)))
2423oveqd 7425 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)) = ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))
2519, 24mpteq12dv 5239 . . . . . . . . . 10 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))) = (π‘₯ ∈ 𝐴 ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))
2615, 16, 25mpoeq123dv 7483 . . . . . . . . 9 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) = (𝑏 ∈ (π‘”π‘β„Ž), π‘Ž ∈ (𝑓𝑁𝑔) ↦ (π‘₯ ∈ 𝐴 ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))
2726csbeq2dv 3900 . . . . . . . 8 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ ⦋(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) = ⦋(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (π‘”π‘β„Ž), π‘Ž ∈ (𝑓𝑁𝑔) ↦ (π‘₯ ∈ 𝐴 ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))
2827csbeq2dv 3900 . . . . . . 7 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))) = ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (π‘”π‘β„Ž), π‘Ž ∈ (𝑓𝑁𝑔) ↦ (π‘₯ ∈ 𝐴 ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))
2914, 8, 28mpoeq123dv 7483 . . . . . 6 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (𝑣 ∈ ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒)), β„Ž ∈ (𝑑 Func 𝑒) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))) = (𝑣 ∈ (𝐡 Γ— 𝐡), β„Ž ∈ 𝐡 ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (π‘”π‘β„Ž), π‘Ž ∈ (𝑓𝑁𝑔) ↦ (π‘₯ ∈ 𝐴 ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))))
30 fucval.x . . . . . . 7 (πœ‘ β†’ βˆ™ = (𝑣 ∈ (𝐡 Γ— 𝐡), β„Ž ∈ 𝐡 ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (π‘”π‘β„Ž), π‘Ž ∈ (𝑓𝑁𝑔) ↦ (π‘₯ ∈ 𝐴 ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))))
3130adantr 481 . . . . . 6 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ βˆ™ = (𝑣 ∈ (𝐡 Γ— 𝐡), β„Ž ∈ 𝐡 ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (π‘”π‘β„Ž), π‘Ž ∈ (𝑓𝑁𝑔) ↦ (π‘₯ ∈ 𝐴 ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩ Β· ((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))))
3229, 31eqtr4d 2775 . . . . 5 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ (𝑣 ∈ ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒)), β„Ž ∈ (𝑑 Func 𝑒) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯))))) = βˆ™ )
3332opeq2d 4880 . . . 4 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒)), β„Ž ∈ (𝑑 Func 𝑒) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩ = ⟨(compβ€˜ndx), βˆ™ ⟩)
349, 13, 33tpeq123d 4752 . . 3 ((πœ‘ ∧ (𝑑 = 𝐢 ∧ 𝑒 = 𝐷)) β†’ {⟨(Baseβ€˜ndx), (𝑑 Func 𝑒)⟩, ⟨(Hom β€˜ndx), (𝑑 Nat 𝑒)⟩, ⟨(compβ€˜ndx), (𝑣 ∈ ((𝑑 Func 𝑒) Γ— (𝑑 Func 𝑒)), β„Ž ∈ (𝑑 Func 𝑒) ↦ ⦋(1st β€˜π‘£) / π‘“β¦Œβ¦‹(2nd β€˜π‘£) / π‘”β¦Œ(𝑏 ∈ (𝑔(𝑑 Nat 𝑒)β„Ž), π‘Ž ∈ (𝑓(𝑑 Nat 𝑒)𝑔) ↦ (π‘₯ ∈ (Baseβ€˜π‘‘) ↦ ((π‘β€˜π‘₯)(⟨((1st β€˜π‘“)β€˜π‘₯), ((1st β€˜π‘”)β€˜π‘₯)⟩(compβ€˜π‘’)((1st β€˜β„Ž)β€˜π‘₯))(π‘Žβ€˜π‘₯)))))⟩} = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), π‘βŸ©, ⟨(compβ€˜ndx), βˆ™ ⟩})
35 fucval.c . . 3 (πœ‘ β†’ 𝐢 ∈ Cat)
36 fucval.d . . 3 (πœ‘ β†’ 𝐷 ∈ Cat)
37 tpex 7733 . . . 4 {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), π‘βŸ©, ⟨(compβ€˜ndx), βˆ™ ⟩} ∈ V
3837a1i 11 . . 3 (πœ‘ β†’ {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), π‘βŸ©, ⟨(compβ€˜ndx), βˆ™ ⟩} ∈ V)
393, 34, 35, 36, 38ovmpod 7559 . 2 (πœ‘ β†’ (𝐢 FuncCat 𝐷) = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), π‘βŸ©, ⟨(compβ€˜ndx), βˆ™ ⟩})
401, 39eqtrid 2784 1 (πœ‘ β†’ 𝑄 = {⟨(Baseβ€˜ndx), 𝐡⟩, ⟨(Hom β€˜ndx), π‘βŸ©, ⟨(compβ€˜ndx), βˆ™ ⟩})
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  Vcvv 3474  β¦‹csb 3893  {ctp 4632  βŸ¨cop 4634   ↦ cmpt 5231   Γ— cxp 5674  β€˜cfv 6543  (class class class)co 7408   ∈ cmpo 7410  1st c1st 7972  2nd c2nd 7973  ndxcnx 17125  Basecbs 17143  Hom chom 17207  compcco 17208  Catccat 17607   Func cfunc 17803   Nat cnat 17891   FuncCat cfuc 17892
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7411  df-oprab 7412  df-mpo 7413  df-fuc 17894
This theorem is referenced by:  fuccofval  17910  fucbas  17911  fuchom  17912  fuchomOLD  17913  fucpropd  17929  catcfuccl  18068  catcfucclOLD  18069
  Copyright terms: Public domain W3C validator