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

Theorem isssc 17703
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.
StepHypRef Expression
1 brssc 17697 . . . 4 (𝐻cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2 fndm 6605 . . . . . . . . . . . 12 (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡))
32adantl 482 . . . . . . . . . . 11 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑡 × 𝑡))
4 isssc.2 . . . . . . . . . . . . 13 (𝜑𝐽 Fn (𝑇 × 𝑇))
54adantr 481 . . . . . . . . . . . 12 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → 𝐽 Fn (𝑇 × 𝑇))
65fndmd 6607 . . . . . . . . . . 11 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑇 × 𝑇))
73, 6eqtr3d 2778 . . . . . . . . . 10 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → (𝑡 × 𝑡) = (𝑇 × 𝑇))
87dmeqd 5861 . . . . . . . . 9 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → dom (𝑡 × 𝑡) = dom (𝑇 × 𝑇))
9 dmxpid 5885 . . . . . . . . 9 dom (𝑡 × 𝑡) = 𝑡
10 dmxpid 5885 . . . . . . . . 9 dom (𝑇 × 𝑇) = 𝑇
118, 9, 103eqtr3g 2799 . . . . . . . 8 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → 𝑡 = 𝑇)
1211ex 413 . . . . . . 7 (𝜑 → (𝐽 Fn (𝑡 × 𝑡) → 𝑡 = 𝑇))
13 id 22 . . . . . . . . . 10 (𝑡 = 𝑇𝑡 = 𝑇)
1413sqxpeqd 5665 . . . . . . . . 9 (𝑡 = 𝑇 → (𝑡 × 𝑡) = (𝑇 × 𝑇))
1514fneq2d 6596 . . . . . . . 8 (𝑡 = 𝑇 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑇 × 𝑇)))
164, 15syl5ibrcom 246 . . . . . . 7 (𝜑 → (𝑡 = 𝑇𝐽 Fn (𝑡 × 𝑡)))
1712, 16impbid 211 . . . . . 6 (𝜑 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝑡 = 𝑇))
1817anbi1d 630 . . . . 5 (𝜑 → ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ (𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧))))
1918exbidv 1924 . . . 4 (𝜑 → (∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧))))
201, 19bitrid 282 . . 3 (𝜑 → (𝐻cat 𝐽 ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧))))
21 isssc.3 . . . 4 (𝜑𝑇𝑉)
22 pweq 4574 . . . . . 6 (𝑡 = 𝑇 → 𝒫 𝑡 = 𝒫 𝑇)
2322rexeqdv 3314 . . . . 5 (𝑡 = 𝑇 → (∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2423ceqsexgv 3604 . . . 4 (𝑇𝑉 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2521, 24syl 17 . . 3 (𝜑 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2620, 25bitrd 278 . 2 (𝜑 → (𝐻cat 𝐽 ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
27 df-rex 3074 . . 3 (∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ ∃𝑠(𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
28 3anass 1095 . . . . . . . 8 ((𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
29 elixp2 8839 . . . . . . . 8 (𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ (𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))
30 vex 3449 . . . . . . . . . . . 12 𝑠 ∈ V
3130, 30xpex 7687 . . . . . . . . . . 11 (𝑠 × 𝑠) ∈ V
32 fnex 7167 . . . . . . . . . . 11 ((𝐻 Fn (𝑠 × 𝑠) ∧ (𝑠 × 𝑠) ∈ V) → 𝐻 ∈ V)
3331, 32mpan2 689 . . . . . . . . . 10 (𝐻 Fn (𝑠 × 𝑠) → 𝐻 ∈ V)
3433adantr 481 . . . . . . . . 9 ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) → 𝐻 ∈ V)
3534pm4.71ri 561 . . . . . . . 8 ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
3628, 29, 353bitr4i 302 . . . . . . 7 (𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))
37 fndm 6605 . . . . . . . . . . . . . 14 (𝐻 Fn (𝑠 × 𝑠) → dom 𝐻 = (𝑠 × 𝑠))
3837adantl 482 . . . . . . . . . . . . 13 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑠 × 𝑠))
39 isssc.1 . . . . . . . . . . . . . . 15 (𝜑𝐻 Fn (𝑆 × 𝑆))
4039adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → 𝐻 Fn (𝑆 × 𝑆))
4140fndmd 6607 . . . . . . . . . . . . 13 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑆 × 𝑆))
4238, 41eqtr3d 2778 . . . . . . . . . . . 12 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → (𝑠 × 𝑠) = (𝑆 × 𝑆))
4342dmeqd 5861 . . . . . . . . . . 11 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → dom (𝑠 × 𝑠) = dom (𝑆 × 𝑆))
44 dmxpid 5885 . . . . . . . . . . 11 dom (𝑠 × 𝑠) = 𝑠
45 dmxpid 5885 . . . . . . . . . . 11 dom (𝑆 × 𝑆) = 𝑆
4643, 44, 453eqtr3g 2799 . . . . . . . . . 10 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → 𝑠 = 𝑆)
4746ex 413 . . . . . . . . 9 (𝜑 → (𝐻 Fn (𝑠 × 𝑠) → 𝑠 = 𝑆))
48 id 22 . . . . . . . . . . . 12 (𝑠 = 𝑆𝑠 = 𝑆)
4948sqxpeqd 5665 . . . . . . . . . . 11 (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆))
5049fneq2d 6596 . . . . . . . . . 10 (𝑠 = 𝑆 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝐻 Fn (𝑆 × 𝑆)))
5139, 50syl5ibrcom 246 . . . . . . . . 9 (𝜑 → (𝑠 = 𝑆𝐻 Fn (𝑠 × 𝑠)))
5247, 51impbid 211 . . . . . . . 8 (𝜑 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝑠 = 𝑆))
5352anbi1d 630 . . . . . . 7 (𝜑 → ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
5436, 53bitrid 282 . . . . . 6 (𝜑 → (𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
5554anbi2d 629 . . . . 5 (𝜑 → ((𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ (𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
56 an12 643 . . . . 5 ((𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
5755, 56bitrdi 286 . . . 4 (𝜑 → ((𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
5857exbidv 1924 . . 3 (𝜑 → (∃𝑠(𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
5927, 58bitrid 282 . 2 (𝜑 → (∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
60 exsimpl 1871 . . . . 5 (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) → ∃𝑠 𝑠 = 𝑆)
61 isset 3458 . . . . 5 (𝑆 ∈ V ↔ ∃𝑠 𝑠 = 𝑆)
6260, 61sylibr 233 . . . 4 (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) → 𝑆 ∈ V)
6362a1i 11 . . 3 (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) → 𝑆 ∈ V))
64 ssexg 5280 . . . . . 6 ((𝑆𝑇𝑇𝑉) → 𝑆 ∈ V)
6564expcom 414 . . . . 5 (𝑇𝑉 → (𝑆𝑇𝑆 ∈ V))
6621, 65syl 17 . . . 4 (𝜑 → (𝑆𝑇𝑆 ∈ V))
6766adantrd 492 . . 3 (𝜑 → ((𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) → 𝑆 ∈ V))
6830elpw 4564 . . . . . . 7 (𝑠 ∈ 𝒫 𝑇𝑠𝑇)
69 sseq1 3969 . . . . . . 7 (𝑠 = 𝑆 → (𝑠𝑇𝑆𝑇))
7068, 69bitrid 282 . . . . . 6 (𝑠 = 𝑆 → (𝑠 ∈ 𝒫 𝑇𝑆𝑇))
7149raleqdv 3313 . . . . . . 7 (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))
72 fvex 6855 . . . . . . . . . 10 (𝐻𝑧) ∈ V
7372elpw 4564 . . . . . . . . 9 ((𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ (𝐻𝑧) ⊆ (𝐽𝑧))
74 fveq2 6842 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
75 df-ov 7360 . . . . . . . . . . 11 (𝑥𝐻𝑦) = (𝐻‘⟨𝑥, 𝑦⟩)
7674, 75eqtr4di 2794 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝑥𝐻𝑦))
77 fveq2 6842 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐽𝑧) = (𝐽‘⟨𝑥, 𝑦⟩))
78 df-ov 7360 . . . . . . . . . . 11 (𝑥𝐽𝑦) = (𝐽‘⟨𝑥, 𝑦⟩)
7977, 78eqtr4di 2794 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐽𝑧) = (𝑥𝐽𝑦))
8076, 79sseq12d 3977 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻𝑧) ⊆ (𝐽𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
8173, 80bitrid 282 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
8281ralxp 5797 . . . . . . 7 (∀𝑧 ∈ (𝑆 × 𝑆)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))
8371, 82bitrdi 286 . . . . . 6 (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
8470, 83anbi12d 631 . . . . 5 (𝑠 = 𝑆 → ((𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
8584ceqsexgv 3604 . . . 4 (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
8685a1i 11 . . 3 (𝜑 → (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))))
8763, 67, 86pm5.21ndd 380 . 2 (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
8826, 59, 873bitrd 304 1 (𝜑 → (𝐻cat 𝐽 ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1087   = wceq 1541  wex 1781  wcel 2106  wral 3064  wrex 3073  Vcvv 3445  wss 3910  𝒫 cpw 4560  cop 4592   class class class wbr 5105   × cxp 5631  dom cdm 5633   Fn wfn 6491  cfv 6496  (class class class)co 7357  Xcixp 8835  cat cssc 17690
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 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-ixp 8836  df-ssc 17693
This theorem is referenced by:  ssc1  17704  ssc2  17705  sscres  17706  ssctr  17708  0ssc  17723  catsubcat  17725  rnghmsscmap2  46261  rnghmsscmap  46262  rhmsscmap2  46307  rhmsscmap  46308  rhmsscrnghm  46314  srhmsubc  46364  fldhmsubc  46372  srhmsubcALTV  46382  fldhmsubcALTV  46390
  Copyright terms: Public domain W3C validator