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

Theorem isssc 17093
 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 17087 . . . 4 (𝐻cat 𝐽 ↔ ∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2 fndm 6458 . . . . . . . . . . . 12 (𝐽 Fn (𝑡 × 𝑡) → dom 𝐽 = (𝑡 × 𝑡))
32adantl 484 . . . . . . . . . . 11 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑡 × 𝑡))
4 isssc.2 . . . . . . . . . . . . 13 (𝜑𝐽 Fn (𝑇 × 𝑇))
54adantr 483 . . . . . . . . . . . 12 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → 𝐽 Fn (𝑇 × 𝑇))
6 fndm 6458 . . . . . . . . . . . 12 (𝐽 Fn (𝑇 × 𝑇) → dom 𝐽 = (𝑇 × 𝑇))
75, 6syl 17 . . . . . . . . . . 11 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → dom 𝐽 = (𝑇 × 𝑇))
83, 7eqtr3d 2861 . . . . . . . . . 10 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → (𝑡 × 𝑡) = (𝑇 × 𝑇))
98dmeqd 5777 . . . . . . . . 9 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → dom (𝑡 × 𝑡) = dom (𝑇 × 𝑇))
10 dmxpid 5803 . . . . . . . . 9 dom (𝑡 × 𝑡) = 𝑡
11 dmxpid 5803 . . . . . . . . 9 dom (𝑇 × 𝑇) = 𝑇
129, 10, 113eqtr3g 2882 . . . . . . . 8 ((𝜑𝐽 Fn (𝑡 × 𝑡)) → 𝑡 = 𝑇)
1312ex 415 . . . . . . 7 (𝜑 → (𝐽 Fn (𝑡 × 𝑡) → 𝑡 = 𝑇))
14 id 22 . . . . . . . . . 10 (𝑡 = 𝑇𝑡 = 𝑇)
1514sqxpeqd 5590 . . . . . . . . 9 (𝑡 = 𝑇 → (𝑡 × 𝑡) = (𝑇 × 𝑇))
1615fneq2d 6450 . . . . . . . 8 (𝑡 = 𝑇 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝐽 Fn (𝑇 × 𝑇)))
174, 16syl5ibrcom 249 . . . . . . 7 (𝜑 → (𝑡 = 𝑇𝐽 Fn (𝑡 × 𝑡)))
1813, 17impbid 214 . . . . . 6 (𝜑 → (𝐽 Fn (𝑡 × 𝑡) ↔ 𝑡 = 𝑇))
1918anbi1d 631 . . . . 5 (𝜑 → ((𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ (𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧))))
2019exbidv 1921 . . . 4 (𝜑 → (∃𝑡(𝐽 Fn (𝑡 × 𝑡) ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧))))
211, 20syl5bb 285 . . 3 (𝜑 → (𝐻cat 𝐽 ↔ ∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧))))
22 isssc.3 . . . 4 (𝜑𝑇𝑉)
23 pweq 4558 . . . . . 6 (𝑡 = 𝑇 → 𝒫 𝑡 = 𝒫 𝑇)
2423rexeqdv 3419 . . . . 5 (𝑡 = 𝑇 → (∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2524ceqsexgv 3650 . . . 4 (𝑇𝑉 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2622, 25syl 17 . . 3 (𝜑 → (∃𝑡(𝑡 = 𝑇 ∧ ∃𝑠 ∈ 𝒫 𝑡𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
2721, 26bitrd 281 . 2 (𝜑 → (𝐻cat 𝐽 ↔ ∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
28 df-rex 3147 . . 3 (∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ ∃𝑠(𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)))
29 3anass 1091 . . . . . . . 8 ((𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
30 elixp2 8468 . . . . . . . 8 (𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ (𝐻 ∈ V ∧ 𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))
31 vex 3500 . . . . . . . . . . . 12 𝑠 ∈ V
3231, 31xpex 7479 . . . . . . . . . . 11 (𝑠 × 𝑠) ∈ V
33 fnex 6983 . . . . . . . . . . 11 ((𝐻 Fn (𝑠 × 𝑠) ∧ (𝑠 × 𝑠) ∈ V) → 𝐻 ∈ V)
3432, 33mpan2 689 . . . . . . . . . 10 (𝐻 Fn (𝑠 × 𝑠) → 𝐻 ∈ V)
3534adantr 483 . . . . . . . . 9 ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) → 𝐻 ∈ V)
3635pm4.71ri 563 . . . . . . . 8 ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝐻 ∈ V ∧ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
3729, 30, 363bitr4i 305 . . . . . . 7 (𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ (𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))
38 fndm 6458 . . . . . . . . . . . . . 14 (𝐻 Fn (𝑠 × 𝑠) → dom 𝐻 = (𝑠 × 𝑠))
3938adantl 484 . . . . . . . . . . . . 13 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑠 × 𝑠))
40 isssc.1 . . . . . . . . . . . . . . 15 (𝜑𝐻 Fn (𝑆 × 𝑆))
4140adantr 483 . . . . . . . . . . . . . 14 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → 𝐻 Fn (𝑆 × 𝑆))
42 fndm 6458 . . . . . . . . . . . . . 14 (𝐻 Fn (𝑆 × 𝑆) → dom 𝐻 = (𝑆 × 𝑆))
4341, 42syl 17 . . . . . . . . . . . . 13 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → dom 𝐻 = (𝑆 × 𝑆))
4439, 43eqtr3d 2861 . . . . . . . . . . . 12 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → (𝑠 × 𝑠) = (𝑆 × 𝑆))
4544dmeqd 5777 . . . . . . . . . . 11 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → dom (𝑠 × 𝑠) = dom (𝑆 × 𝑆))
46 dmxpid 5803 . . . . . . . . . . 11 dom (𝑠 × 𝑠) = 𝑠
47 dmxpid 5803 . . . . . . . . . . 11 dom (𝑆 × 𝑆) = 𝑆
4845, 46, 473eqtr3g 2882 . . . . . . . . . 10 ((𝜑𝐻 Fn (𝑠 × 𝑠)) → 𝑠 = 𝑆)
4948ex 415 . . . . . . . . 9 (𝜑 → (𝐻 Fn (𝑠 × 𝑠) → 𝑠 = 𝑆))
50 id 22 . . . . . . . . . . . 12 (𝑠 = 𝑆𝑠 = 𝑆)
5150sqxpeqd 5590 . . . . . . . . . . 11 (𝑠 = 𝑆 → (𝑠 × 𝑠) = (𝑆 × 𝑆))
5251fneq2d 6450 . . . . . . . . . 10 (𝑠 = 𝑆 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝐻 Fn (𝑆 × 𝑆)))
5340, 52syl5ibrcom 249 . . . . . . . . 9 (𝜑 → (𝑠 = 𝑆𝐻 Fn (𝑠 × 𝑠)))
5449, 53impbid 214 . . . . . . . 8 (𝜑 → (𝐻 Fn (𝑠 × 𝑠) ↔ 𝑠 = 𝑆))
5554anbi1d 631 . . . . . . 7 (𝜑 → ((𝐻 Fn (𝑠 × 𝑠) ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
5637, 55syl5bb 285 . . . . . 6 (𝜑 → (𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
5756anbi2d 630 . . . . 5 (𝜑 → ((𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ (𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
58 an12 643 . . . . 5 ((𝑠 ∈ 𝒫 𝑇 ∧ (𝑠 = 𝑆 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))))
5957, 58syl6bb 289 . . . 4 (𝜑 → ((𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ (𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
6059exbidv 1921 . . 3 (𝜑 → (∃𝑠(𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧)) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
6128, 60syl5bb 285 . 2 (𝜑 → (∃𝑠 ∈ 𝒫 𝑇𝐻X𝑧 ∈ (𝑠 × 𝑠)𝒫 (𝐽𝑧) ↔ ∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))))
62 exsimpl 1868 . . . . 5 (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) → ∃𝑠 𝑠 = 𝑆)
63 isset 3509 . . . . 5 (𝑆 ∈ V ↔ ∃𝑠 𝑠 = 𝑆)
6462, 63sylibr 236 . . . 4 (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) → 𝑆 ∈ V)
6564a1i 11 . . 3 (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) → 𝑆 ∈ V))
66 ssexg 5230 . . . . . 6 ((𝑆𝑇𝑇𝑉) → 𝑆 ∈ V)
6766expcom 416 . . . . 5 (𝑇𝑉 → (𝑆𝑇𝑆 ∈ V))
6822, 67syl 17 . . . 4 (𝜑 → (𝑆𝑇𝑆 ∈ V))
6968adantrd 494 . . 3 (𝜑 → ((𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)) → 𝑆 ∈ V))
7031elpw 4546 . . . . . . 7 (𝑠 ∈ 𝒫 𝑇𝑠𝑇)
71 sseq1 3995 . . . . . . 7 (𝑠 = 𝑆 → (𝑠𝑇𝑆𝑇))
7270, 71syl5bb 285 . . . . . 6 (𝑠 = 𝑆 → (𝑠 ∈ 𝒫 𝑇𝑆𝑇))
7351raleqdv 3418 . . . . . . 7 (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ ∀𝑧 ∈ (𝑆 × 𝑆)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)))
74 fvex 6686 . . . . . . . . . 10 (𝐻𝑧) ∈ V
7574elpw 4546 . . . . . . . . 9 ((𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ (𝐻𝑧) ⊆ (𝐽𝑧))
76 fveq2 6673 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝐻‘⟨𝑥, 𝑦⟩))
77 df-ov 7162 . . . . . . . . . . 11 (𝑥𝐻𝑦) = (𝐻‘⟨𝑥, 𝑦⟩)
7876, 77syl6eqr 2877 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐻𝑧) = (𝑥𝐻𝑦))
79 fveq2 6673 . . . . . . . . . . 11 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐽𝑧) = (𝐽‘⟨𝑥, 𝑦⟩))
80 df-ov 7162 . . . . . . . . . . 11 (𝑥𝐽𝑦) = (𝐽‘⟨𝑥, 𝑦⟩)
8179, 80syl6eqr 2877 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ → (𝐽𝑧) = (𝑥𝐽𝑦))
8278, 81sseq12d 4003 . . . . . . . . 9 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻𝑧) ⊆ (𝐽𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
8375, 82syl5bb 285 . . . . . . . 8 (𝑧 = ⟨𝑥, 𝑦⟩ → ((𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
8483ralxp 5715 . . . . . . 7 (∀𝑧 ∈ (𝑆 × 𝑆)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))
8573, 84syl6bb 289 . . . . . 6 (𝑠 = 𝑆 → (∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧) ↔ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))
8672, 85anbi12d 632 . . . . 5 (𝑠 = 𝑆 → ((𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧)) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
8786ceqsexgv 3650 . . . 4 (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
8887a1i 11 . . 3 (𝜑 → (𝑆 ∈ V → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦)))))
8965, 69, 88pm5.21ndd 383 . 2 (𝜑 → (∃𝑠(𝑠 = 𝑆 ∧ (𝑠 ∈ 𝒫 𝑇 ∧ ∀𝑧 ∈ (𝑠 × 𝑠)(𝐻𝑧) ∈ 𝒫 (𝐽𝑧))) ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
9027, 61, 893bitrd 307 1 (𝜑 → (𝐻cat 𝐽 ↔ (𝑆𝑇 ∧ ∀𝑥𝑆𝑦𝑆 (𝑥𝐻𝑦) ⊆ (𝑥𝐽𝑦))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1536  ∃wex 1779   ∈ wcel 2113  ∀wral 3141  ∃wrex 3142  Vcvv 3497   ⊆ wss 3939  𝒫 cpw 4542  ⟨cop 4576   class class class wbr 5069   × cxp 5556  dom cdm 5558   Fn wfn 6353  ‘cfv 6358  (class class class)co 7159  Xcixp 8464   ⊆cat cssc 17080 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796  ax-rep 5193  ax-sep 5206  ax-nul 5213  ax-pow 5269  ax-pr 5333  ax-un 7464 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-mo 2621  df-eu 2653  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-ne 3020  df-ral 3146  df-rex 3147  df-reu 3148  df-rab 3150  df-v 3499  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-pw 4544  df-sn 4571  df-pr 4573  df-op 4577  df-uni 4842  df-iun 4924  df-br 5070  df-opab 5132  df-mpt 5150  df-id 5463  df-xp 5564  df-rel 5565  df-cnv 5566  df-co 5567  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571  df-iota 6317  df-fun 6360  df-fn 6361  df-f 6362  df-f1 6363  df-fo 6364  df-f1o 6365  df-fv 6366  df-ov 7162  df-ixp 8465  df-ssc 17083 This theorem is referenced by:  ssc1  17094  ssc2  17095  sscres  17096  ssctr  17098  0ssc  17110  catsubcat  17112  rnghmsscmap2  44251  rnghmsscmap  44252  rhmsscmap2  44297  rhmsscmap  44298  rhmsscrnghm  44304  srhmsubc  44354  fldhmsubc  44362  srhmsubcALTV  44372  fldhmsubcALTV  44380
 Copyright terms: Public domain W3C validator