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

Theorem isssc 17532
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 17526 . . . 4 (𝐻cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2 fndm 6536 . . . . . . . . . . . 12 (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡))
32adantl 482 . . . . . . . . . . 11 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑡 × 𝑡))
4 isssc.2 . . . . . . . . . . . . 13 (𝜑𝐽 Fn (𝑇 × 𝑇))
54adantr 481 . . . . . . . . . . . 12 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → 𝐽 Fn (𝑇 × 𝑇))
65fndmd 6538 . . . . . . . . . . 11 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑇 × 𝑇))
73, 6eqtr3d 2780 . . . . . . . . . 10 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → (𝑡 × 𝑡) = (𝑇 × 𝑇))
87dmeqd 5814 . . . . . . . . 9 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → dom (𝑡 × 𝑡) = dom (𝑇 × 𝑇))
9 dmxpid 5839 . . . . . . . . 9 dom (𝑡 × 𝑡) = 𝑡
10 dmxpid 5839 . . . . . . . . 9 dom (𝑇 × 𝑇) = 𝑇
118, 9, 103eqtr3g 2801 . . . . . . . 8 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → 𝑡 = 𝑇)
1211ex 413 . . . . . . 7 (𝜑 → (𝐽 Fn (𝑡 × 𝑡) → 𝑡 = 𝑇))
13 id 22 . . . . . . . . . 10 (𝑡 = 𝑇𝑡 = 𝑇)
1413sqxpeqd 5621 . . . . . . . . 9 (𝑡 = 𝑇 → (𝑡 × 𝑡) = (𝑇 × 𝑇))
1514fneq2d 6527 . . . . . . . 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 4549 . . . . . 6 (𝑡 = 𝑇 → 𝒫 𝑡 = 𝒫 𝑇)
2322rexeqdv 3349 . . . . 5 (𝑡 = 𝑇 → (∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2423ceqsexgv 3584 . . . 4 (𝑇𝑉 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2521, 24syl 17 . . 3 (𝜑 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2620, 25bitrd 278 . 2 (𝜑 → (𝐻cat 𝐽 ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
27 df-rex 3070 . . 3 (∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ ∃𝑠(𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
28 3anass 1094 . . . . . . . 8 ((𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
29 elixp2 8689 . . . . . . . 8 (𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ (𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))
30 vex 3436 . . . . . . . . . . . 12 𝑠 ∈ V
3130, 30xpex 7603 . . . . . . . . . . 11 (𝑠 × 𝑠) ∈ V
32 fnex 7093 . . . . . . . . . . 11 ((𝐻 Fn (𝑠 × 𝑠) ∧ (𝑠 × 𝑠) ∈ V) → 𝐻 ∈ V)
3331, 32mpan2 688 . . . . . . . . . 10 (𝐻 Fn (𝑠 × 𝑠) → 𝐻 ∈ V)
3433adantr 481 . . . . . . . . 9 ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) → 𝐻 ∈ V)
3534pm4.71ri 561 . . . . . . . 8 ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
3628, 29, 353bitr4i 303 . . . . . . 7 (𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))
37 fndm 6536 . . . . . . . . . . . . . 14 (𝐻 Fn (𝑠 × 𝑠) → dom 𝐻 = (𝑠 × 𝑠))
3837adantl 482 . . . . . . . . . . . . 13 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑠 × 𝑠))
39 isssc.1 . . . . . . . . . . . . . . 15 (𝜑𝐻 Fn (𝑆 × 𝑆))
4039adantr 481 . . . . . . . . . . . . . 14 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → 𝐻 Fn (𝑆 × 𝑆))
4140fndmd 6538 . . . . . . . . . . . . 13 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑆 × 𝑆))
4238, 41eqtr3d 2780 . . . . . . . . . . . 12 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → (𝑠 × 𝑠) = (𝑆 × 𝑆))
4342dmeqd 5814 . . . . . . . . . . 11 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → dom (𝑠 × 𝑠) = dom (𝑆 × 𝑆))
44 dmxpid 5839 . . . . . . . . . . 11 dom (𝑠 × 𝑠) = 𝑠
45 dmxpid 5839 . . . . . . . . . . 11 dom (𝑆 × 𝑆) = 𝑆
4643, 44, 453eqtr3g 2801 . . . . . . . . . 10 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → 𝑠 = 𝑆)
4746ex 413 . . . . . . . . 9 (𝜑 → (𝐻 Fn (𝑠 × 𝑠) → 𝑠 = 𝑆))
48 id 22 . . . . . . . . . . . 12 (𝑠 = 𝑆𝑠 = 𝑆)
4948sqxpeqd 5621 . . . . . . . . . . 11 (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆))
5049fneq2d 6527 . . . . . . . . . 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 642 . . . . 5 ((𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
5755, 56bitrdi 287 . . . 4 (𝜑 → ((𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
5857exbidv 1924 . . 3 (𝜑 → (∃𝑠(𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
5927, 58bitrid 282 . 2 (𝜑 → (∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
60 exsimpl 1871 . . . . 5 (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) → ∃𝑠 𝑠 = 𝑆)
61 isset 3445 . . . . 5 (𝑆 ∈ V ↔ ∃𝑠 𝑠 = 𝑆)
6260, 61sylibr 233 . . . 4 (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) → 𝑆 ∈ V)
6362a1i 11 . . 3 (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) → 𝑆 ∈ V))
64 ssexg 5247 . . . . . 6 ((𝑆𝑇𝑇𝑉) → 𝑆 ∈ V)
6564expcom 414 . . . . 5 (𝑇𝑉 → (𝑆𝑇𝑆 ∈ V))
6621, 65syl 17 . . . 4 (𝜑 → (𝑆𝑇𝑆 ∈ V))
6766adantrd 492 . . 3 (𝜑 → ((𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) → 𝑆 ∈ V))
6830elpw 4537 . . . . . . 7 (𝑠 ∈ 𝒫 𝑇𝑠𝑇)
69 sseq1 3946 . . . . . . 7 (𝑠 = 𝑆 → (𝑠𝑇𝑆𝑇))
7068, 69bitrid 282 . . . . . 6 (𝑠 = 𝑆 → (𝑠 ∈ 𝒫 𝑇𝑆𝑇))
7149raleqdv 3348 . . . . . . 7 (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))
72 fvex 6787 . . . . . . . . . 10 (𝐻𝑧) ∈ V
7372elpw 4537 . . . . . . . . 9 ((𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ (𝐻𝑧) ⊆ (𝐽𝑧))
74 fveq2 6774 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
75 df-ov 7278 . . . . . . . . . . 11 (𝑥𝐻𝑦) = (𝐻‘⟨𝑥, 𝑦⟩)
7674, 75eqtr4di 2796 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝑥𝐻𝑦))
77 fveq2 6774 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐽𝑧) = (𝐽‘⟨𝑥, 𝑦⟩))
78 df-ov 7278 . . . . . . . . . . 11 (𝑥𝐽𝑦) = (𝐽‘⟨𝑥, 𝑦⟩)
7977, 78eqtr4di 2796 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐽𝑧) = (𝑥𝐽𝑦))
8076, 79sseq12d 3954 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻𝑧) ⊆ (𝐽𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
8173, 80bitrid 282 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
8281ralxp 5750 . . . . . . 7 (∀𝑧 ∈ (𝑆 × 𝑆)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))
8371, 82bitrdi 287 . . . . . 6 (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
8470, 83anbi12d 631 . . . . 5 (𝑠 = 𝑆 → ((𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
8584ceqsexgv 3584 . . . 4 (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
8685a1i 11 . . 3 (𝜑 → (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))))
8763, 67, 86pm5.21ndd 381 . 2 (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
8826, 59, 873bitrd 305 1 (𝜑 → (𝐻cat 𝐽 ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1539  wex 1782  wcel 2106  wral 3064  wrex 3065  Vcvv 3432  wss 3887  𝒫 cpw 4533  cop 4567   class class class wbr 5074   × cxp 5587  dom cdm 5589   Fn wfn 6428  cfv 6433  (class class class)co 7275  Xcixp 8685  cat cssc 17519
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  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 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-ixp 8686  df-ssc 17522
This theorem is referenced by:  ssc1  17533  ssc2  17534  sscres  17535  ssctr  17537  0ssc  17552  catsubcat  17554  rnghmsscmap2  45531  rnghmsscmap  45532  rhmsscmap2  45577  rhmsscmap  45578  rhmsscrnghm  45584  srhmsubc  45634  fldhmsubc  45642  srhmsubcALTV  45652  fldhmsubcALTV  45660
  Copyright terms: Public domain W3C validator